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  7607  limensuci  7712  phplem4  7718  unfi  7805  fiint  7815  cdaen  8570  isfin1-3  8783  prlem934  9428  0idsr  9491  1idsr  9492  00sr  9493  addresr  9532  mulresr  9533  reclt1  10460  crne0  10549  nominpos  10796  expnass  12275  faclbnd2  12371  crim  12959  sqrlem1  13087  sqrlem7  13093  sqrt00  13108  sqreulem  13203  mulcn2  13429  ege2le3  13836  sin02gt0  13938  opoe  14346  oddprm  14350  pythagtriplem2  14352  pythagtriplem3  14353  pythagtriplem16  14365  pythagtrip  14369  pc1  14390  prmlem0  14602  acsfn0  15076  mgpress  17278  abvneg  17609  pmatcollpw3  19411  leordtval2  19839  txswaphmeo  20431  iccntr  21451  dvlipcn  22520  sinq34lt0t  23027  cosordlem  23043  efif1olem3  23056  basellem3  23481  ppiub  23604  bposlem9  23692  lgsne0  23733  lgsdinn0  23740  chebbnd1  23782  constr1trl  24716  constr2trl  24727  usgrcyclnl2  24767  4cycl4dv  24793  2spontn0vne  25013  eupath2lem3  25105  mayete3i  26772  mayete3iOLD  26773  lnop0  27011  nmcexi  27071  nmoptrii  27139  nmopcoadji  27146  hstle1  27271  hst0  27278  strlem5  27300  jplem1  27313  cnvoprab  27696  lgamgulmlem2  28747  subfacp1lem5  28803  wfisg  29463  frinsg  29499  limsucncmpi  30072  dvasin  30265  fdc  30400  eldioph3b  30860  sinhpcosh  33236
  Copyright terms: Public domain W3C validator