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

Theorem mpanr12 668
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 666 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 654 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  2dom  7182  limensuci  7286  phplem4  7292  unfi  7377  fiint  7386  cdaen  8058  isfin1-3  8271  prlem934  8915  0idsr  8977  1idsr  8978  00sr  8979  addresr  9018  mulresr  9019  reclt1  9910  crne0  9998  nominpos  10209  expnass  11491  faclbnd2  11587  crim  11925  sqrlem1  12053  sqrlem7  12059  sqr00  12074  sqreulem  12168  mulcn2  12394  ege2le3  12697  sin02gt0  12798  opoe  13190  oddprm  13194  pythagtriplem2  13196  pythagtriplem3  13197  pythagtriplem16  13209  pythagtrip  13213  pc1  13234  prmlem0  13433  acsfn0  13890  mgpress  15664  abvneg  15927  leordtval2  17281  txswaphmeo  17842  iccntr  18857  dvlipcn  19883  sinq34lt0t  20422  cosordlem  20438  efif1olem3  20451  basellem3  20870  ppiub  20993  bposlem9  21081  lgsne0  21122  lgsdinn0  21129  chebbnd1  21171  trls  21541  constr1trl  21593  constr2wlk  21603  constr2trl  21604  usgrcyclnl2  21633  4cycl4dv  21659  eupath2lem3  21706  mayete3i  23235  mayete3iOLD  23236  lnop0  23474  nmcexi  23534  nmoptrii  23602  nmopcoadji  23609  hstle1  23734  hst0  23741  strlem5  23763  jplem1  23776  lgamgulmlem2  24819  subfacp1lem5  24875  wfisg  25489  frinsg  25525  limsucncmpi  26200  heicant  26253  fdc  26463  eldioph3b  26837  2spontn0vne  28419  sinhpcosh  28557
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 179  df-an 362
  Copyright terms: Public domain W3C validator