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  1657  mo  2167  moexex  2214  mob  2949  limuni3  4645  issref  5058  sotri2  5074  sotri3  5075  relresfld  5201  poxp  6229  soxp  6230  tfrlem5  6398  tz7.49  6459  omwordri  6572  odi  6579  omass  6580  oewordri  6592  nndi  6623  nnmass  6624  r1sdom  7448  tz9.12lem3  7463  cardlim  7607  carduni  7616  alephordi  7703  alephval3  7739  domtriomlem  8070  axdc3lem2  8079  axdc3lem4  8081  axcclem  8085  zorn2lem5  8129  zorn2lem6  8130  axdclem2  8149  alephval2  8196  gruen  8436  grur1a  8443  grothomex  8453  nqereu  8555  distrlem5pr  8653  psslinpr  8657  ltaprlem  8670  suplem1pr  8678  lbreu  9706  caubnd  11844  algcvga  12751  algfx  12752  spwmo  14337  fiinopn  16649  hausnei  17058  hausnei2  17083  cmpsublem  17128  cmpsub  17129  fcfneii  17734  ppiublem1  20443  chintcli  21912  h1datomi  22162  strlem3a  22834  hstrlem3a  22842  mdexchi  22917  cvbr4i  22949  mdsymlem4  22988  mdsymlem6  22990  3jaodd  24067  frr3g  24282  ifscgr  24669  rspc2edv  24974  11st22nd  25056  prj1b  25090  prj3  25091  iscomb  25345  grpodivfo  25385  ltrooo  25415  muldisc  25492  intopcoaconb  25551  islimrs4  25593  bwt2  25603  addcanrg  25678  negveud  25679  negveudr  25680  intvconlem1  25714  cmpassoh  25812  cmpmon  25826  tartarmap  25899  carinttar  25913  pgapspf2  26064  nbssntrs  26158  wepwsolem  27149  ee233  28337
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator