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  ax12b  1696  dvelimv  1975  mo  2260  moexex  2307  mob  3059  limuni3  4772  issref  5187  sotri2  5203  sotri3  5204  relresfld  5336  poxp  6394  soxp  6395  tfrlem5  6577  tz7.49  6638  omwordri  6751  odi  6758  omass  6759  oewordri  6771  nndi  6802  nnmass  6803  r1sdom  7633  tz9.12lem3  7648  cardlim  7792  carduni  7801  alephordi  7888  alephval3  7924  domtriomlem  8255  axdc3lem2  8264  axdc3lem4  8266  axcclem  8270  zorn2lem5  8313  zorn2lem6  8314  axdclem2  8333  alephval2  8380  gruen  8620  grur1a  8627  grothomex  8637  nqereu  8739  distrlem5pr  8837  psslinpr  8841  ltaprlem  8854  suplem1pr  8862  lbreu  9890  caubnd  12089  algcvga  12997  algfx  12998  spwmo  14585  fiinopn  16897  hausnei  17314  hausnei2  17339  cmpsublem  17384  cmpsub  17385  fcfneii  17990  ppiublem1  20853  nb3graprlem1  21326  cusgrasize2inds  21352  wlkdvspthlem  21455  chintcli  22681  h1datomi  22931  strlem3a  23603  hstrlem3a  23611  mdexchi  23686  cvbr4i  23718  mdsymlem4  23757  mdsymlem6  23759  3jaodd  24947  frr3g  25304  ifscgr  25692  wepwsolem  26807  vdgn1frgrav2  27780  frgrancvvdeqlemB  27790  frgrancvvdeqlemC  27791  ad5ant23  27896  ad5ant24  27897  ad5ant25  27898  ee233  27945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator