Other Derived Rules

Derived rules discussed in the text are not necessarily available for use in the CPL. The following rules are discussed in the text, but are not currently available in the CPL (move your mouse pointer over any rule to see the rule definition):

conjunction Assoc.& L Assoc.& R Distr.& Distr.& C Idem.& I Idem.& E  
∀& &∀ ∃&        
disjunction Distr.v Distr.v C Assoc.v L Assoc.v R Idem.v I Idem.v E Cut
v∀ v∃ ∃v ∀DS L ∀DS R ∃DS L ∃DS R
conditional Contra. Exp.& Exp.→ ¬→ I ¬→ E    
∀→ ∀→∃ ∃→ ∀HS ∀MT    
negation Def.∀ I Def.∀ E Def.∃ I Def.∃ E    
biconditional Comm. ↔ RE ∀↔ ∀RE      
Other RBV (∀) RBV (∃) ∀∀ ∃∃ ∃∀