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  6933  limensuci  7037  phplem4  7043  unfi  7124  fiint  7133  cdaen  7799  isfin1-3  8012  prlem934  8657  0idsr  8719  1idsr  8720  00sr  8721  addresr  8760  mulresr  8761  reclt1  9651  crne0  9739  nominpos  9948  expnass  11208  faclbnd2  11304  crim  11600  sqrlem1  11728  sqrlem7  11734  sqr00  11749  sqreulem  11843  mulcn2  12069  ege2le3  12371  sin02gt0  12472  opoe  12864  oddprm  12868  pythagtriplem2  12870  pythagtriplem3  12871  pythagtriplem16  12883  pythagtrip  12887  pc1  12908  prmlem0  13107  acsfn0  13562  mgpress  15336  abvneg  15599  leordtval2  16942  txswaphmeo  17496  iccntr  18326  dvlipcn  19341  sinq34lt0t  19877  cosordlem  19893  efif1olem3  19906  basellem3  20320  ppiub  20443  bposlem9  20531  lgsne0  20572  lgsdinn0  20579  chebbnd1  20621  mayete3i  22307  mayete3iOLD  22308  lnop0  22546  nmcexi  22606  nmoptrii  22674  nmopcoadji  22681  hstle1  22806  hst0  22813  strlem5  22835  jplem1  22848  subfacp1lem5  23715  eupath2lem3  23903  wfisg  24209  frinsg  24245  limsucncmpi  24884  fdc  26455  eldioph3b  26844  sinhpcosh  28210
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