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 3

This theorem is referenced by:  3expd 848  uniiunlem 2122  elpwunsn 2902  onint 2996  findsg 3147  tfindsg 3152  tfrlem9 3904  tz7.49 3944  oaordi 4164  odi 4194  oaabs 4236  php 4493  fiint 4534  aceq6b 4714  zorn2lem6 4765  zorn2lem7 4766  carduni 4830  mulcanpi 4999  ltexprlem7 5120  xrsupsslem 6023  xrinfmsslem 6024  supxrunb1 6036  supxrunb2 6037  qbtwnre 6216  seq1rn2 6258  elfz4t 6407  seqzrn2 6488  reccnv 7153  cnsscnp 7711  lmle 7895  bcthlem33 7965  ipblnfi 8447  spwmo 8580  projlem28 9129  sumdmdlem 10252  cmpmon 10585

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

Copyright terms: Public domain