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

Theorem com3r 75
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 74 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
32com12 29 1  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com13  76  com3l  77  com14  84  exp3a  426  mo  2280  moexex  2327  mob  3080  limuni3  4795  issref  5210  sotri2  5226  sotri3  5227  relresfld  5359  poxp  6421  soxp  6422  tfrlem5  6604  tz7.49  6665  omwordri  6778  odi  6785  omass  6786  oewordri  6798  nndi  6829  nnmass  6830  r1sdom  7660  tz9.12lem3  7675  cardlim  7819  carduni  7828  alephordi  7915  alephval3  7951  domtriomlem  8282  axdc3lem2  8291  axdc3lem4  8293  axcclem  8297  zorn2lem5  8340  zorn2lem6  8341  axdclem2  8360  alephval2  8407  gruen  8647  grur1a  8654  grothomex  8664  nqereu  8766  distrlem5pr  8864  psslinpr  8868  ltaprlem  8881  suplem1pr  8889  lbreu  9918  caubnd  12121  algcvga  13029  algfx  13030  spwmo  14617  fiinopn  16933  hausnei  17350  hausnei2  17375  cmpsublem  17420  cmpsub  17421  fcfneii  18026  ppiublem1  20943  nb3graprlem1  21417  cusgrasize2inds  21443  wlkdvspthlem  21564  chintcli  22790  h1datomi  23040  strlem3a  23712  hstrlem3a  23720  mdexchi  23795  cvbr4i  23827  mdsymlem4  23866  mdsymlem6  23868  3jaodd  25125  frr3g  25498  ifscgr  25886  wepwsolem  27010  usgra2wlkspth  28042  vdgn1frgrav2  28135  frgrancvvdeqlemB  28145  frgrancvvdeqlemC  28146  ad5ant23  28268  ad5ant24  28269  ad5ant25  28270  ee233  28317
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator