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  2310  moexex  2357  mob  3125  limuni3  4867  issref  5282  sotri2  5298  sotri3  5299  relresfld  5431  poxp  6494  soxp  6495  tfrlem5  6677  tz7.49  6738  omwordri  6851  odi  6858  omass  6859  oewordri  6871  nndi  6902  nnmass  6903  r1sdom  7736  tz9.12lem3  7751  cardlim  7897  carduni  7906  alephordi  7993  alephval3  8029  domtriomlem  8360  axdc3lem2  8369  axdc3lem4  8371  axcclem  8375  zorn2lem5  8418  zorn2lem6  8419  axdclem2  8438  alephval2  8485  gruen  8725  grur1a  8732  grothomex  8742  nqereu  8844  distrlem5pr  8942  psslinpr  8946  ltaprlem  8959  suplem1pr  8967  lbreu  9996  caubnd  12200  algcvga  13108  algfx  13109  spwmo  14696  fiinopn  17012  hausnei  17430  hausnei2  17455  cmpsublem  17500  cmpsub  17501  bwth  17511  fcfneii  18107  ppiublem1  21024  nb3graprlem1  21498  cusgrasize2inds  21524  wlkdvspthlem  21645  chintcli  22871  h1datomi  23121  strlem3a  23793  hstrlem3a  23801  mdexchi  23876  cvbr4i  23908  mdsymlem4  23947  mdsymlem6  23949  3jaodd  25203  frr3g  25616  ifscgr  26013  wepwsolem  27228  usgra2wlkspth  28444  vdgn1frgrav2  28589  frgrancvvdeqlemB  28599  frgrancvvdeqlemC  28600  ad5ant23  28722  ad5ant24  28723  ad5ant25  28724  ee233  28774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator