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

Theorem com3r 76
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 75 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
32com12 30 1  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com13  77  com3l  78  com14  85  exp3a  427  mo  2305  moexex  2352  mob  3118  limuni3  4835  issref  5250  sotri2  5266  sotri3  5267  relresfld  5399  poxp  6461  soxp  6462  tfrlem5  6644  tz7.49  6705  omwordri  6818  odi  6825  omass  6826  oewordri  6838  nndi  6869  nnmass  6870  r1sdom  7703  tz9.12lem3  7718  cardlim  7864  carduni  7873  alephordi  7960  alephval3  7996  domtriomlem  8327  axdc3lem2  8336  axdc3lem4  8338  axcclem  8342  zorn2lem5  8385  zorn2lem6  8386  axdclem2  8405  alephval2  8452  gruen  8692  grur1a  8699  grothomex  8709  nqereu  8811  distrlem5pr  8909  psslinpr  8913  ltaprlem  8926  suplem1pr  8934  lbreu  9963  caubnd  12167  algcvga  13075  algfx  13076  spwmo  14663  fiinopn  16979  hausnei  17397  hausnei2  17422  cmpsublem  17467  cmpsub  17468  bwth  17478  fcfneii  18074  ppiublem1  20991  nb3graprlem1  21465  cusgrasize2inds  21491  wlkdvspthlem  21612  chintcli  22838  h1datomi  23088  strlem3a  23760  hstrlem3a  23768  mdexchi  23843  cvbr4i  23875  mdsymlem4  23914  mdsymlem6  23916  3jaodd  25173  frr3g  25586  ifscgr  25983  wepwsolem  27130  usgra2wlkspth  28346  vdgn1frgrav2  28491  frgrancvvdeqlemB  28501  frgrancvvdeqlemC  28502  ad5ant23  28624  ad5ant24  28625  ad5ant25  28626  ee233  28676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator