Theorem com3r 82

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 81	. 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  83  com3l  84  com14  91  expd  437  ad5ant23  1242  ad5ant24  1243  ad5ant25  1244  mob  3190  issref  5170  sotri2  5186  sotri3  5187  relresfld  5319  limuni3  6632  poxp  6858  soxp  6859  tz7.49  7112  omwordri  7223  odi  7230  omass  7231  oewordri  7243  nndi  7274  nnmass  7275  r1sdom  8192  tz9.12lem3  8207  cardlim  8353  carduni  8362  alephordi  8451  alephval3  8487  domtriomlem  8818  axdc3lem2  8827  axdc3lem4  8829  axcclem  8833  zorn2lem5  8876  zorn2lem6  8877  axdclem2  8896  alephval2  8943  gruen  9183  grur1a  9190  grothomex  9200  nqereu  9300  distrlem5pr  9398  psslinpr  9402  ltaprlem  9415  suplem1pr  9423  lbreu  10502  fleqceilz  12026  caubnd  13360  algcvga  14476  algfx  14477  gsummatr01lem3  19619  fiinopn  19868  hausnei  20281  hausnei2  20306  cmpsublem  20351  cmpsub  20352  fcfneii  20989  ppiublem1  24067  nb3graprlem1  25116  cusgrasize2inds  25142  wlkdvspthlem  25274  usgra2wlkspth  25286  clwwlkprop  25435  clwwlkgt0  25436  clwlkisclwwlklem1  25452  clwwlkf  25459  vdgn1frgrav2  25691  frgrancvvdeqlemB  25703  frgrancvvdeqlemC  25704  frgraregord013  25783  chintcli  26921  h1datomi  27171  strlem3a  27842  hstrlem3a  27850  mdexchi  27925  cvbr4i  27957  mdsymlem4  27996  mdsymlem6  27998  3jaodd  30293  frr3g  30459  ifscgr  30755  bj-mo3OLD  31358  wepwsolem  35813  rp-fakeimass  36069  ee233  36789  iccpartgt  38554  nb3grprlem1  39185  cusgrsize2inds  39242  ldepspr  39859