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 4559  fiintOLD 4560  aceq5 4740  ltexprlem7 5148  reclem3pr 5158  infpnlem1 7506  cnpco 7769  cncnplem4 7777  projlem28 9213  spansncv 9597  cdj3lem2b 10364  uninqs 10441  cdrci 10494  homcard 10539  fipfil2 10564  fipfil2OLD 10565  neifil 10568  efilcp 10572  efilcpOLD 10573  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  cmpmon 10743  icmpmon 10744

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

Copyright terms: Public domain