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 3

This theorem is referenced by:  com4l 39  fiint 4572  fiintOLD 4573  aceq5 4750  ltexprlem7 5160  reclem3pr 5170  infpnlem1 7507  cnpco 7766  cncnplem4 7774  projlem28 9208  spansncv 9592  cdj3lem2b 10359  uninqs 10436  cdrci 10480  homcard 10525  fipfil2 10550  neifil 10553  efilcp 10556  efilcp2 10561  cnfilca 10562  cmpmon 10714  icmpmon 10715

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

Copyright terms: Public domain