com45 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > com45		Unicode version

Theorem com45 89

Description: Commutation of antecedents. Swap 4th and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.)

**Hypothesis**
Ref	Expression
com5.1

**Assertion**
Ref	Expression
com45

**Proof of Theorem com45**
Step	Hyp	Ref	Expression
1		com5.1	. 2
2		pm2.04 82	. 2
3	1, 2	syl8 71	1

Colors of variables: wff set class

Syntax hints:

wi 4

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7

This theorem is referenced by: com35 90 com25 91 com5l 92