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 850  uniiunlem 2132  elpwunsn 2912  onint 3006  findsg 3157  tfindsg 3162  tfrlem9 3919  tz7.49 3959  oaordi 4180  odi 4210  oaabs 4252  php 4513  fiint 4559  fiintOLD 4560  aceq6b 4742  zorn2lem6 4793  zorn2lem7 4794  carduni 4858  mulcanpi 5027  ltexprlem7 5148  xrsupsslem 6076  xrinfmsslem 6077  supxrunb1 6089  supxrunb2 6090  qbtwnre 6278  seq1rn2 6321  elfz4t 6475  seqzrn2 6556  reccnv 7218  cnsscnp 7772  lmle 7960  bcthlem33 8031  ipblnfi 8516  spwmo 8656  projlem28 9213  sumdmdlem 10345  cmpmon 10743

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

Copyright terms: Public domain