Theorem com4r 94

Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.)

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 93	. 2 |- ( ch -> ( th -> ( ph -> ( ps -> ta ) ) ) )
3	2	com4l 92	1 |- ( th -> ( ph -> ( ps -> ( ch -> ta ) ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com15  101  3imp3i2an  1278  3expd  1284  elpwunsn  4224  onint  6995  tfindsg  7060  findsg  7093  tfrlem9  7481  tz7.49  7540  oaordi  7626  odi  7659  nnaordi  7698  nndi  7703  php  8144  fiint  8237  carduni  8807  dfac2  8953  axcclem  9279  zorn2lem6  9323  zorn2lem7  9324  grur1a  9641  mulcanpi  9722  ltexprlem7  9864  axpre-sup  9990  xrsupsslem  12137  xrinfmsslem  12138  supxrunb1  12149  supxrunb2  12150  mulgnnass  17576  mulgnnassOLD  17577  fiinopn  20706  axcont  25856  sumdmdlem  29277  matunitlindflem1  33405  ee33VD  39115