Theorem com14 38

Description: Commutation of antecedents. Swap 1st and 4th.

Hypothesis

Ref	Expression
com4.1	|- (ph -> (ps -> (ch -> (th -> ta ))))

Assertion

Ref	Expression
com14	|- (th -> (ps -> (ch -> (ph -> ta ))))

Proof of Theorem com14

Step	Hyp	Ref	Expression
1		com4.1	. . . 4 |- (ph -> (ps -> (ch -> (th -> ta ))))
2	1	com34 36	. . 3 |- (ph -> (ps -> (th -> (ch -> ta ))))
3	2	com13 33	. 2 |- (th -> (ps -> (ph -> (ch -> ta ))))
4	3	com34 36	1 |- (th -> (ps -> (ch -> (ph -> ta ))))

Syntax hints:   -> wi 2

This theorem is referenced by:  com4l 39  aceq5 3563  ltexprlem7 3942  reclem3pr 3952  projlem28 5220  spansncv 5542

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org