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  1655  mo  2165  moexex  2212  mob  2947  limuni3  4643  issref  5056  sotri2  5072  sotri3  5073  relresfld  5199  poxp  6227  soxp  6228  tfrlem5  6396  tz7.49  6457  omwordri  6570  odi  6577  omass  6578  oewordri  6590  nndi  6621  nnmass  6622  r1sdom  7446  tz9.12lem3  7461  cardlim  7605  carduni  7614  alephordi  7701  alephval3  7737  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axcclem  8083  zorn2lem5  8127  zorn2lem6  8128  axdclem2  8147  alephval2  8194  gruen  8434  grur1a  8441  grothomex  8451  nqereu  8553  distrlem5pr  8651  psslinpr  8655  ltaprlem  8668  suplem1pr  8676  lbreu  9704  caubnd  11842  algcvga  12749  algfx  12750  spwmo  14335  fiinopn  16647  hausnei  17056  hausnei2  17081  cmpsublem  17126  cmpsub  17127  fcfneii  17732  ppiublem1  20441  chintcli  21910  h1datomi  22160  strlem3a  22832  hstrlem3a  22840  mdexchi  22915  cvbr4i  22947  mdsymlem4  22986  mdsymlem6  22988  3jaodd  24065  frr3g  24280  ifscgr  24667  rspc2edv  24963  11st22nd  25045  prj1b  25079  prj3  25080  iscomb  25334  grpodivfo  25374  ltrooo  25404  muldisc  25481  intopcoaconb  25540  islimrs4  25582  bwt2  25592  addcanrg  25667  negveud  25668  negveudr  25669  intvconlem1  25703  cmpassoh  25801  cmpmon  25815  tartarmap  25888  carinttar  25902  pgapspf2  26053  nbssntrs  26147  wepwsolem  27138  ee233  28281
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator