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

Theorem mpanr12 667
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 665 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 653 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  2dom  7138  limensuci  7242  phplem4  7248  unfi  7333  fiint  7342  cdaen  8009  isfin1-3  8222  prlem934  8866  0idsr  8928  1idsr  8929  00sr  8930  addresr  8969  mulresr  8970  reclt1  9861  crne0  9949  nominpos  10160  expnass  11441  faclbnd2  11537  crim  11875  sqrlem1  12003  sqrlem7  12009  sqr00  12024  sqreulem  12118  mulcn2  12344  ege2le3  12647  sin02gt0  12748  opoe  13140  oddprm  13144  pythagtriplem2  13146  pythagtriplem3  13147  pythagtriplem16  13159  pythagtrip  13163  pc1  13184  prmlem0  13383  acsfn0  13840  mgpress  15614  abvneg  15877  leordtval2  17230  txswaphmeo  17790  iccntr  18805  dvlipcn  19831  sinq34lt0t  20370  cosordlem  20386  efif1olem3  20399  basellem3  20818  ppiub  20941  bposlem9  21029  lgsne0  21070  lgsdinn0  21077  chebbnd1  21119  trls  21489  constr1trl  21541  constr2wlk  21551  constr2trl  21552  usgrcyclnl2  21581  4cycl4dv  21607  eupath2lem3  21654  mayete3i  23183  mayete3iOLD  23184  lnop0  23422  nmcexi  23482  nmoptrii  23550  nmopcoadji  23557  hstle1  23682  hst0  23689  strlem5  23711  jplem1  23724  lgamgulmlem2  24767  subfacp1lem5  24823  wfisg  25423  frinsg  25459  limsucncmpi  26099  fdc  26339  eldioph3b  26713  2spontn0vne  28084  sinhpcosh  28197
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator