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 849  uniiunlem 2129  elpwunsn 2908  onint 3002  findsg 3153  tfindsg 3158  tfrlem9 3914  tz7.49 3954  oaordi 4173  odi 4203  oaabs 4245  php 4502  fiint 4543  aceq6b 4725  zorn2lem6 4776  zorn2lem7 4777  carduni 4841  mulcanpi 5010  ltexprlem7 5131  xrsupsslem 6033  xrinfmsslem 6034  supxrunb1 6046  supxrunb2 6047  qbtwnre 6228  seq1rn2 6271  elfz4t 6420  seqzrn2 6501  reccnv 7170  cnsscnp 7732  lmle 7922  bcthlem33 7993  ipblnfi 8475  spwmo 8613  projlem28 9168  sumdmdlem 10301  cmpmon 10657

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

Copyright terms: Public domain