Theorem com4r 41

Description: Commutation of antecedents. Rotate right.

Hypothesis

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

Assertion

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

Proof of Theorem com4r

Step	Hyp	Ref	Expression
1		com4.1	. . 3 |- (ph -> (ps -> (ch -> (th -> ta ))))
2	1	com4t 40	. 2 |- (ch -> (th -> (ph -> (ps -> ta ))))
3	2	com4l 39	1 |- (th -> (ph -> (ps -> (ch -> ta ))))

Syntax hints:   -> wi 2

This theorem is referenced by:  onint 2261  findsg 2398  tfindsg 2402  tfrlem2 2950  tfrlem9 2957  oaordi 3148  nndi 3180  php 3409  fiint 3445  aceq6b 3565  zornlem6 3608  zornlem7 3609  carduni 3664  mulcanpi 3821  ltexprlem7 3942  qbtwnre 4650  seqrn 4673  projlem28 5220  sumdmdlem 5786

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

metamath.org