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

Theorem mpanr12 685
Description: An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.)
Hypotheses
Ref Expression
mpanr12.1  |-  ps
mpanr12.2  |-  ch
mpanr12.3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Assertion
Ref Expression
mpanr12  |-  ( ph  ->  th )

Proof of Theorem mpanr12
StepHypRef Expression
1 mpanr12.2 . 2  |-  ch
2 mpanr12.1 . . 3  |-  ps
3 mpanr12.3 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
42, 3mpanr1 683 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 671 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  2dom  7397  limensuci  7502  phplem4  7508  unfi  7594  fiint  7603  cdaen  8357  isfin1-3  8570  prlem934  9217  0idsr  9279  1idsr  9280  00sr  9281  addresr  9320  mulresr  9321  reclt1  10242  crne0  10330  nominpos  10576  expnass  11986  faclbnd2  12082  crim  12619  sqrlem1  12747  sqrlem7  12753  sqr00  12768  sqreulem  12862  mulcn2  13088  ege2le3  13390  sin02gt0  13491  opoe  13893  oddprm  13897  pythagtriplem2  13899  pythagtriplem3  13900  pythagtriplem16  13912  pythagtrip  13916  pc1  13937  prmlem0  14148  acsfn0  14613  mgpress  16617  abvneg  16934  leordtval2  18831  txswaphmeo  19393  iccntr  20413  dvlipcn  21481  sinq34lt0t  21986  cosordlem  22002  efif1olem3  22015  basellem3  22435  ppiub  22558  bposlem9  22646  lgsne0  22687  lgsdinn0  22694  chebbnd1  22736  trls  23450  constr1trl  23502  constr2wlk  23512  constr2trl  23513  usgrcyclnl2  23542  4cycl4dv  23568  eupath2lem3  23615  mayete3i  25146  mayete3iOLD  25147  lnop0  25385  nmcexi  25445  nmoptrii  25513  nmopcoadji  25520  hstle1  25645  hst0  25652  strlem5  25674  jplem1  25687  lgamgulmlem2  27031  subfacp1lem5  27087  wfisg  27685  frinsg  27721  limsucncmpi  28306  dvasin  28499  fdc  28660  eldioph3b  29122  2spontn0vne  30425  sinhpcosh  31094
  Copyright terms: Public domain W3C validator