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

Theorem mpanr12 689
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 687 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 675 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  wfisg  5425  2dom  7640  limensuci  7745  phplem4  7751  unfi  7835  fiint  7845  cdaen  8592  isfin1-3  8805  prlem934  9447  0idsr  9510  1idsr  9511  00sr  9512  addresr  9551  mulresr  9552  reclt1  10490  crne0  10591  nominpos  10838  expnass  12366  faclbnd2  12462  crim  13146  sqrlem1  13274  sqrlem7  13280  sqrt00  13295  sqreulem  13390  mulcn2  13626  ege2le3  14111  sin02gt0  14213  opoe  14713  oddprm  14717  pythagtriplem2  14719  pythagtriplem3  14720  pythagtriplem16  14732  pythagtrip  14736  pc1  14757  prmlem0  15029  acsfn0  15510  mgpress  17662  abvneg  17990  pmatcollpw3  19732  leordtval2  20152  txswaphmeo  20744  iccntr  21743  dvlipcn  22820  sinq34lt0t  23326  cosordlem  23342  efif1olem3  23355  lgamgulmlem2  23817  basellem3  23869  ppiub  23992  bposlem9  24080  lgsne0  24121  lgsdinn0  24128  chebbnd1  24170  constr1trl  25160  constr2trl  25171  usgrcyclnl2  25211  4cycl4dv  25237  2spontn0vne  25457  eupath2lem3  25549  mayete3i  27213  lnop0  27451  nmcexi  27511  nmoptrii  27579  nmopcoadji  27586  hstle1  27711  hst0  27718  strlem5  27740  jplem1  27753  cnvoprab  28148  subfacp1lem5  29692  frinsg  30267  limsucncmpi  30887  poimirlem15  31659  dvasin  31732  fdc  31778  eldioph3b  35316  sinhpcosh  39234
  Copyright terms: Public domain W3C validator