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

Theorem mpanr12 666
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 664 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 652 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  2dom  6949  limensuci  7053  phplem4  7059  unfi  7140  fiint  7149  cdaen  7815  isfin1-3  8028  prlem934  8673  0idsr  8735  1idsr  8736  00sr  8737  addresr  8776  mulresr  8777  reclt1  9667  crne0  9755  nominpos  9964  expnass  11224  faclbnd2  11320  crim  11616  sqrlem1  11744  sqrlem7  11750  sqr00  11765  sqreulem  11859  mulcn2  12085  ege2le3  12387  sin02gt0  12488  opoe  12880  oddprm  12884  pythagtriplem2  12886  pythagtriplem3  12887  pythagtriplem16  12899  pythagtrip  12903  pc1  12924  prmlem0  13123  acsfn0  13578  mgpress  15352  abvneg  15615  leordtval2  16958  txswaphmeo  17512  iccntr  18342  dvlipcn  19357  sinq34lt0t  19893  cosordlem  19909  efif1olem3  19922  basellem3  20336  ppiub  20459  bposlem9  20547  lgsne0  20588  lgsdinn0  20595  chebbnd1  20637  mayete3i  22323  mayete3iOLD  22324  lnop0  22562  nmcexi  22622  nmoptrii  22690  nmopcoadji  22697  hstle1  22822  hst0  22829  strlem5  22851  jplem1  22864  subfacp1lem5  23730  eupath2lem3  23918  wfisg  24280  frinsg  24316  limsucncmpi  24956  itg2addnc  25005  fdc  26558  eldioph3b  26947  trls  28335  usgrcyclnl2  28387  4cycl4dv  28413  sinhpcosh  28464
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 177  df-an 360
  Copyright terms: Public domain W3C validator