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

Theorem com3r 73
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 72 . 2  |-  ( ph  ->  ( ch  ->  ( ps  ->  th ) ) )
32com12 27 1  |-  ( ch 
->  ( ph  ->  ( ps  ->  th ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com13  74  com3l  75  com14  82  exp3a  425  ax12b  1674  mo  2178  moexex  2225  mob  2960  limuni3  4659  issref  5072  sotri2  5088  sotri3  5089  relresfld  5215  poxp  6243  soxp  6244  tfrlem5  6412  tz7.49  6473  omwordri  6586  odi  6593  omass  6594  oewordri  6606  nndi  6637  nnmass  6638  r1sdom  7462  tz9.12lem3  7477  cardlim  7621  carduni  7630  alephordi  7717  alephval3  7753  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  axcclem  8099  zorn2lem5  8143  zorn2lem6  8144  axdclem2  8163  alephval2  8210  gruen  8450  grur1a  8457  grothomex  8467  nqereu  8569  distrlem5pr  8667  psslinpr  8671  ltaprlem  8684  suplem1pr  8692  lbreu  9720  caubnd  11858  algcvga  12765  algfx  12766  spwmo  14351  fiinopn  16663  hausnei  17072  hausnei2  17097  cmpsublem  17142  cmpsub  17143  fcfneii  17748  ppiublem1  20457  chintcli  21926  h1datomi  22176  strlem3a  22848  hstrlem3a  22856  mdexchi  22931  cvbr4i  22963  mdsymlem4  23002  mdsymlem6  23004  3jaodd  24080  frr3g  24351  ifscgr  24739  rspc2edv  25066  11st22nd  25148  prj1b  25182  prj3  25183  iscomb  25437  grpodivfo  25477  ltrooo  25507  muldisc  25584  intopcoaconb  25643  islimrs4  25685  bwt2  25695  addcanrg  25770  negveud  25771  negveudr  25772  intvconlem1  25806  cmpassoh  25904  cmpmon  25918  tartarmap  25991  carinttar  26005  pgapspf2  26156  nbssntrs  26250  wepwsolem  27241  nb3graprlem1  28287  wlkdvspthlem  28365  ee233  28580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator