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  2302  moexex  2349  mob  3108  limuni3  4823  issref  5238  sotri2  5254  sotri3  5255  relresfld  5387  poxp  6449  soxp  6450  tfrlem5  6632  tz7.49  6693  omwordri  6806  odi  6813  omass  6814  oewordri  6826  nndi  6857  nnmass  6858  r1sdom  7689  tz9.12lem3  7704  cardlim  7848  carduni  7857  alephordi  7944  alephval3  7980  domtriomlem  8311  axdc3lem2  8320  axdc3lem4  8322  axcclem  8326  zorn2lem5  8369  zorn2lem6  8370  axdclem2  8389  alephval2  8436  gruen  8676  grur1a  8683  grothomex  8693  nqereu  8795  distrlem5pr  8893  psslinpr  8897  ltaprlem  8910  suplem1pr  8918  lbreu  9947  caubnd  12150  algcvga  13058  algfx  13059  spwmo  14646  fiinopn  16962  hausnei  17380  hausnei2  17405  cmpsublem  17450  cmpsub  17451  bwth  17461  fcfneii  18057  ppiublem1  20974  nb3graprlem1  21448  cusgrasize2inds  21474  wlkdvspthlem  21595  chintcli  22821  h1datomi  23071  strlem3a  23743  hstrlem3a  23751  mdexchi  23826  cvbr4i  23858  mdsymlem4  23897  mdsymlem6  23899  3jaodd  25156  frr3g  25535  ifscgr  25926  wepwsolem  27053  usgra2wlkspth  28182  vdgn1frgrav2  28275  frgrancvvdeqlemB  28285  frgrancvvdeqlemC  28286  ad5ant23  28408  ad5ant24  28409  ad5ant25  28410  ee233  28457
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator