Theorem com3r 79

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 78	. 2 |- ( ph -> ( ch -> ( ps -> th ) ) )
3	2	com12 31	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  80  com3l  81  com14  88  expd  436  mo3OLD  2316  moOLD  2322  moexexOLD  2367  mob  3280  issref  5373  sotri2  5389  sotri3  5390  relresfld  5527  limuni3  6660  poxp  6887  soxp  6888  tz7.49  7102  omwordri  7213  odi  7220  omass  7221  oewordri  7233  nndi  7264  nnmass  7265  r1sdom  8183  tz9.12lem3  8198  cardlim  8344  carduni  8353  alephordi  8446  alephval3  8482  domtriomlem  8813  axdc3lem2  8822  axdc3lem4  8824  axcclem  8828  zorn2lem5  8871  zorn2lem6  8872  axdclem2  8891  alephval2  8938  gruen  9181  grur1a  9188  grothomex  9198  nqereu  9298  distrlem5pr  9396  psslinpr  9400  ltaprlem  9413  suplem1pr  9421  lbreu  10484  fleqceilz  11939  caubnd  13142  algcvga  14058  algfx  14059  gsummatr01lem3  18921  fiinopn  19172  hausnei  19590  hausnei2  19615  cmpsublem  19660  cmpsub  19661  bwthOLD  19672  fcfneii  20268  ppiublem1  23200  nb3graprlem1  24115  cusgrasize2inds  24141  wlkdvspthlem  24273  usgra2wlkspth  24285  clwwlkprop  24434  clwwlkgt0  24435  clwlkisclwwlklem1  24451  clwwlkf  24458  vdgn1frgrav2  24691  frgrancvvdeqlemB  24703  frgrancvvdeqlemC  24704  frgraregord013  24783  chintcli  25913  h1datomi  26163  strlem3a  26835  hstrlem3a  26843  mdexchi  26918  cvbr4i  26950  mdsymlem4  26989  mdsymlem6  26991  3jaodd  28554  frr3g  28951  ifscgr  29259  wepwsolem  30582  ldepspr  32024  ad5ant23  32192  ad5ant24  32193  ad5ant25  32194  ee233  32245