Theorem com4l 39

Description: Commutation of antecedents. Rotate left. (The proof was shortened by O'Cat, 15-Aug-2004.)

Hypothesis

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

Assertion

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

Proof of Theorem com4l

Step	Hyp	Ref	Expression
1		com4.1	. . 3 |- (ph -> (ps -> (ch -> (th -> ta))))
2	1	com14 38	. 2 |- (th -> (ps -> (ch -> (ph -> ta))))
3	2	com3l 34	1 |- (ps -> (ch -> (th -> (ph -> ta))))

Syntax hints:   -> wi 3

This theorem is referenced by:  com4t 40  com4r 41  3impd 847  trel 2687  reuuni4 2887  onint 3006  tfrlem1 3911  oalimcl 4194  oeordsuc 4221  zorn2lem7 4794  prlem934 5139  mulcant 5690  ioojoint 6416  expnbndt 6654  facwordit 6944  cvgratlem2 7251  unbenlem 7504  tgss2t 7637  ssbl 7855  opnin 7869  xplmi 7973  bcthlem20 8018  bcthlem33 8031  spansncol 9491  osumlem4 9581  atcvat4 10324  sumdmdlem 10345  fiv 10482  fivOLD 10483  top2ind 10548  filint2 10574  filint2OLD 10575  fisub 10576  fisubOLD 10577

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

Copyright terms: Public domain