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  2310  mob  3267  issref  5370  sotri2  5386  sotri3  5387  relresfld  5524  limuni3  6672  poxp  6897  soxp  6898  tz7.49  7112  omwordri  7223  odi  7230  omass  7231  oewordri  7243  nndi  7274  nnmass  7275  r1sdom  8195  tz9.12lem3  8210  cardlim  8356  carduni  8365  alephordi  8458  alephval3  8494  domtriomlem  8825  axdc3lem2  8834  axdc3lem4  8836  axcclem  8840  zorn2lem5  8883  zorn2lem6  8884  axdclem2  8903  alephval2  8950  gruen  9193  grur1a  9200  grothomex  9210  nqereu  9310  distrlem5pr  9408  psslinpr  9412  ltaprlem  9425  suplem1pr  9433  lbreu  10499  fleqceilz  11960  caubnd  13170  algcvga  14085  algfx  14086  gsummatr01lem3  19032  fiinopn  19283  hausnei  19702  hausnei2  19727  cmpsublem  19772  cmpsub  19773  bwthOLD  19784  fcfneii  20411  ppiublem1  23349  nb3graprlem1  24323  cusgrasize2inds  24349  wlkdvspthlem  24481  usgra2wlkspth  24493  clwwlkprop  24642  clwwlkgt0  24643  clwlkisclwwlklem1  24659  clwwlkf  24666  vdgn1frgrav2  24898  frgrancvvdeqlemB  24910  frgrancvvdeqlemC  24911  frgraregord013  24990  chintcli  26121  h1datomi  26371  strlem3a  27043  hstrlem3a  27051  mdexchi  27126  cvbr4i  27158  mdsymlem4  27197  mdsymlem6  27199  3jaodd  28964  frr3g  29361  ifscgr  29669  wepwsolem  30962  ldepspr  32809  ad5ant23  32969  ad5ant24  32970  ad5ant25  32971  ee233  33022  rp-fakeimass  37439