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  7585  limensuci  7690  phplem4  7696  unfi  7783  fiint  7793  cdaen  8549  isfin1-3  8762  prlem934  9407  0idsr  9470  1idsr  9471  00sr  9472  addresr  9511  mulresr  9512  reclt1  10436  crne0  10525  nominpos  10771  expnass  12237  faclbnd2  12333  crim  12907  sqrlem1  13035  sqrlem7  13041  sqrt00  13056  sqreulem  13151  mulcn2  13377  ege2le3  13683  sin02gt0  13784  opoe  14190  oddprm  14194  pythagtriplem2  14196  pythagtriplem3  14197  pythagtriplem16  14209  pythagtrip  14213  pc1  14234  prmlem0  14445  acsfn0  14911  mgpress  16942  abvneg  17266  pmatcollpw3  19052  leordtval2  19479  txswaphmeo  20041  iccntr  21061  dvlipcn  22130  sinq34lt0t  22635  cosordlem  22651  efif1olem3  22664  basellem3  23084  ppiub  23207  bposlem9  23295  lgsne0  23336  lgsdinn0  23343  chebbnd1  23385  trls  24214  constr1trl  24266  constr2wlk  24276  constr2trl  24277  usgrcyclnl2  24317  4cycl4dv  24343  2spontn0vne  24563  eupath2lem3  24655  mayete3i  26322  mayete3iOLD  26323  lnop0  26561  nmcexi  26621  nmoptrii  26689  nmopcoadji  26696  hstle1  26821  hst0  26828  strlem5  26850  jplem1  26863  lgamgulmlem2  28212  subfacp1lem5  28268  wfisg  28866  frinsg  28902  limsucncmpi  29487  dvasin  29680  fdc  29841  eldioph3b  30302  sinhpcosh  32215
  Copyright terms: Public domain W3C validator