Theorem com4l 39

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

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 2

This theorem is referenced by:  com4t 40  com4r 41  reuuni4 1959  trel 2048  supmo 2156  onint 2261  tfrlem1 2949  tfrlem8 2956  oalimcl 3162  zornlem7 3609  prlem934 3933  spansncol 5473  osumlem4 5533  atcvat4 5775  sumdmdlem 5786

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

metamath.org