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  442  ad5ant23  1254  ad5ant24  1255  ad5ant25  1256  mob  3231  issref  5231  sotri2  5247  sotri3  5248  relresfld  5380  limuni3  6705  poxp  6934  soxp  6935  tz7.49  7187  omwordri  7298  odi  7305  omass  7306  oewordri  7318  nndi  7349  nnmass  7350  r1sdom  8270  tz9.12lem3  8285  cardlim  8431  carduni  8440  alephordi  8530  alephval3  8566  domtriomlem  8897  axdc3lem2  8906  axdc3lem4  8908  axcclem  8912  zorn2lem5  8955  zorn2lem6  8956  axdclem2  8975  alephval2  9022  gruen  9262  grur1a  9269  grothomex  9279  nqereu  9379  distrlem5pr  9477  psslinpr  9481  ltaprlem  9494  suplem1pr  9502  lbreu  10583  fleqceilz  12112  caubnd  13469  algcvga  14586  algfx  14587  gsummatr01lem3  19730  fiinopn  19979  hausnei  20392  hausnei2  20417  cmpsublem  20462  cmpsub  20463  fcfneii  21100  ppiublem1  24178  nb3graprlem1  25227  cusgrasize2inds  25253  wlkdvspthlem  25385  usgra2wlkspth  25397  clwwlkprop  25546  clwwlkgt0  25547  clwlkisclwwlklem1  25563  clwwlkf  25570  vdgn1frgrav2  25802  frgrancvvdeqlemB  25814  frgrancvvdeqlemC  25815  frgraregord013  25894  chintcli  27032  h1datomi  27282  strlem3a  27953  hstrlem3a  27961  mdexchi  28036  cvbr4i  28068  mdsymlem4  28107  mdsymlem6  28109  3jaodd  30394  frr3g  30561  ifscgr  30859  bj-mo3OLD  31491  wepwsolem  35944  rp-fakeimass  36200  ee233  36919  iccpartgt  38778  nb3grprlem1  39503  cusgrsize2inds  39563  1wlk1walk  39696  ldepspr  40538