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  2299  moOLD  2305  moexexOLD  2350  mob  3140  issref  5210  sotri2  5226  sotri3  5227  relresfld  5363  limuni3  6462  poxp  6683  soxp  6684  tz7.49  6899  omwordri  7010  odi  7017  omass  7018  oewordri  7030  nndi  7061  nnmass  7062  r1sdom  7980  tz9.12lem3  7995  cardlim  8141  carduni  8150  alephordi  8243  alephval3  8279  domtriomlem  8610  axdc3lem2  8619  axdc3lem4  8621  axcclem  8625  zorn2lem5  8668  zorn2lem6  8669  axdclem2  8688  alephval2  8735  gruen  8978  grur1a  8985  grothomex  8995  nqereu  9097  distrlem5pr  9195  psslinpr  9199  ltaprlem  9212  suplem1pr  9220  lbreu  10279  fleqceilz  11692  caubnd  12845  algcvga  13753  algfx  13754  gsummatr01lem3  18462  fiinopn  18513  hausnei  18931  hausnei2  18956  cmpsublem  19001  cmpsub  19002  bwthOLD  19013  fcfneii  19609  ppiublem1  22540  nb3graprlem1  23358  cusgrasize2inds  23384  wlkdvspthlem  23505  chintcli  24733  h1datomi  24983  strlem3a  25655  hstrlem3a  25663  mdexchi  25738  cvbr4i  25770  mdsymlem4  25809  mdsymlem6  25811  3jaodd  27369  frr3g  27766  ifscgr  28074  wepwsolem  29392  usgra2wlkspth  30296  clwwlkprop  30431  clwwlkgt0  30432  clwlkisclwwlklem1  30447  clwwlkf  30454  vdgn1frgrav2  30617  frgrancvvdeqlemB  30629  frgrancvvdeqlemC  30630  frgraregord013  30709  ldepspr  31005  ad5ant23  31169  ad5ant24  31170  ad5ant25  31171  ee233  31222