MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com3r Structured version   Visualization version   Unicode version

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
StepHypRef Expression
1 com3.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
21com23 81 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
32com12 32 1  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator