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  1656  mo  2166  moexex  2213  mob  2948  limuni3  4642  issref  5055  sotri2  5071  sotri3  5072  relresfld  5197  poxp  6189  soxp  6190  tfrlem5  6392  tz7.49  6453  omwordri  6566  odi  6573  omass  6574  oewordri  6586  nndi  6617  nnmass  6618  r1sdom  7442  tz9.12lem3  7457  cardlim  7601  carduni  7610  alephordi  7697  alephval3  7733  domtriomlem  8064  axdc3lem2  8073  axdc3lem4  8075  axcclem  8079  zorn2lem5  8123  zorn2lem6  8124  axdclem2  8143  alephval2  8190  gruen  8430  grur1a  8437  grothomex  8447  nqereu  8549  distrlem5pr  8647  psslinpr  8651  ltaprlem  8664  suplem1pr  8672  lbreu  9700  caubnd  11838  algcvga  12745  algfx  12746  spwmo  14331  fiinopn  16643  hausnei  17052  hausnei2  17077  cmpsublem  17122  cmpsub  17123  fcfneii  17728  ppiublem1  20437  chintcli  21906  h1datomi  22156  strlem3a  22828  hstrlem3a  22836  mdexchi  22911  cvbr4i  22943  mdsymlem4  22982  mdsymlem6  22984  3jaodd  23472  frr3g  23684  ifscgr  24077  rspc2edv  24373  11st22nd  24455  prj1b  24489  prj3  24490  iscomb  24745  grpodivfo  24785  ltrooo  24815  muldisc  24892  intopcoaconb  24951  islimrs4  24993  bwt2  25003  addcanrg  25078  negveud  25079  negveudr  25080  intvconlem1  25114  cmpassoh  25212  cmpmon  25226  tartarmap  25299  carinttar  25313  pgapspf2  25464  nbssntrs  25558  wepwsolem  26549  ee233  27564
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator