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

Theorem mpanr12 680
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 678 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 666 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  7378  limensuci  7483  phplem4  7489  unfi  7575  fiint  7584  cdaen  8338  isfin1-3  8551  prlem934  9198  0idsr  9260  1idsr  9261  00sr  9262  addresr  9301  mulresr  9302  reclt1  10223  crne0  10311  nominpos  10557  expnass  11967  faclbnd2  12063  crim  12600  sqrlem1  12728  sqrlem7  12734  sqr00  12749  sqreulem  12843  mulcn2  13069  ege2le3  13371  sin02gt0  13472  opoe  13874  oddprm  13878  pythagtriplem2  13880  pythagtriplem3  13881  pythagtriplem16  13893  pythagtrip  13897  pc1  13918  prmlem0  14129  acsfn0  14594  mgpress  16592  abvneg  16899  leordtval2  18775  txswaphmeo  19337  iccntr  20357  dvlipcn  21425  sinq34lt0t  21930  cosordlem  21946  efif1olem3  21959  basellem3  22379  ppiub  22502  bposlem9  22590  lgsne0  22631  lgsdinn0  22638  chebbnd1  22680  trls  23370  constr1trl  23422  constr2wlk  23432  constr2trl  23433  usgrcyclnl2  23462  4cycl4dv  23488  eupath2lem3  23535  mayete3i  25066  mayete3iOLD  25067  lnop0  25305  nmcexi  25365  nmoptrii  25433  nmopcoadji  25440  hstle1  25565  hst0  25572  strlem5  25594  jplem1  25607  lgamgulmlem2  26946  subfacp1lem5  27002  wfisg  27599  frinsg  27635  limsucncmpi  28221  dvasin  28405  fdc  28566  eldioph3b  29028  2spontn0vne  30331  sinhpcosh  30916
  Copyright terms: Public domain W3C validator