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  434  mo3OLD  2325  mob  3278  issref  5368  sotri2  5384  sotri3  5385  relresfld  5517  limuni3  6660  poxp  6885  soxp  6886  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  9179  grur1a  9186  grothomex  9196  nqereu  9296  distrlem5pr  9394  psslinpr  9398  ltaprlem  9411  suplem1pr  9419  lbreu  10488  fleqceilz  11963  caubnd  13273  algcvga  14292  algfx  14293  gsummatr01lem3  19326  fiinopn  19577  hausnei  19996  hausnei2  20021  cmpsublem  20066  cmpsub  20067  fcfneii  20704  ppiublem1  23675  nb3graprlem1  24653  cusgrasize2inds  24679  wlkdvspthlem  24811  usgra2wlkspth  24823  clwwlkprop  24972  clwwlkgt0  24973  clwlkisclwwlklem1  24989  clwwlkf  24996  vdgn1frgrav2  25228  frgrancvvdeqlemB  25240  frgrancvvdeqlemC  25241  frgraregord013  25320  chintcli  26447  h1datomi  26697  strlem3a  27369  hstrlem3a  27377  mdexchi  27452  cvbr4i  27484  mdsymlem4  27523  mdsymlem6  27525  3jaodd  29332  frr3g  29626  ifscgr  29922  wepwsolem  31226  ldepspr  33328  ad5ant23  33623  ad5ant24  33624  ad5ant25  33625  ee233  33676  rp-fakeimass  38150