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):

	Assoc.& L	Assoc.& R	Distr.&	Distr.& C	Idem.& I	Idem.& E
	∀&	&∀	∃&
	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
	Contra.	Exp.&	Exp.→	¬→ I	¬→ E
	∀→	∀→∃	∃→	∀HS	∀MT
	Def.∀ I	Def.∀ E	Def.∃ I	Def.∃ E
	Comm. ↔	RE	∀↔	∀RE
Other	RBV (∀)	RBV (∃)	∀∀	∃∃	∃∀