Theorem com3r 87

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

Hypothesis

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

Assertion

Ref	Expression
com3r	|- ( ch -> ( ph -> ( ps -> th ) ) )

Proof of Theorem com3r

Step	Hyp	Ref	Expression
1		com3.1	. . 3 |- ( ph -> ( ps -> ( ch -> th ) ) )
2	1	com23 86	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
3	2	com12 32	1 |- ( ch -> ( ph -> ( ps -> th ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  com13  88  com3l  89  com14  96  expd  452  ad5ant23  1304  ad5ant24  1305  ad5ant25  1306  mob  3388  otiunsndisj  4980  issref  5509  sotri2  5525  sotri3  5526  relresfld  5662  limuni3  7052  poxp  7289  soxp  7290  tz7.49  7540  omwordri  7652  odi  7659  omass  7660  oewordri  7672  nndi  7703  nnmass  7704  r1sdom  8637  tz9.12lem3  8652  cardlim  8798  carduni  8807  alephordi  8897  alephval3  8933  domtriomlem  9264  axdc3lem2  9273  axdc3lem4  9275  axcclem  9279  zorn2lem5  9322  zorn2lem6  9323  axdclem2  9342  alephval2  9394  gruen  9634  grur1a  9641  grothomex  9651  nqereu  9751  distrlem5pr  9849  psslinpr  9853  ltaprlem  9866  suplem1pr  9874  lbreu  10973  fleqceilz  12653  caubnd  14098  divconjdvds  15037  algcvga  15292  algfx  15293  gsummatr01lem3  20463  fiinopn  20706  hausnei  21132  hausnei2  21157  cmpsublem  21202  cmpsub  21203  fcfneii  21841  ppiublem1  24927  nb3grprlem1  26282  cusgrsize2inds  26349  wlk1walk  26535  clwlkclwwlklem2  26901  clwwlksf  26915  vdgn1frgrv2  27160  frgrncvvdeqlem8  27170  frgrncvvdeqlem9  27171  frgrreggt1  27251  frgrregord013  27253  chintcli  28190  h1datomi  28440  strlem3a  29111  hstrlem3a  29119  mdexchi  29194  cvbr4i  29226  mdsymlem4  29265  mdsymlem6  29267  3jaodd  31595  frr3g  31779  ifscgr  32151  bj-mo3OLD  32832  wepwsolem  37612  rp-fakeimass  37857  ee233  38725  iccpartgt  41363  lighneal  41528  ldepspr  42262