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

Theorem mpanr12 667
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 665 . 2  |-  ( (
ph  /\  ch )  ->  th )
51, 4mpan2 653 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  2dom  7171  limensuci  7275  phplem4  7281  unfi  7366  fiint  7375  cdaen  8045  isfin1-3  8258  prlem934  8902  0idsr  8964  1idsr  8965  00sr  8966  addresr  9005  mulresr  9006  reclt1  9897  crne0  9985  nominpos  10196  expnass  11478  faclbnd2  11574  crim  11912  sqrlem1  12040  sqrlem7  12046  sqr00  12061  sqreulem  12155  mulcn2  12381  ege2le3  12684  sin02gt0  12785  opoe  13177  oddprm  13181  pythagtriplem2  13183  pythagtriplem3  13184  pythagtriplem16  13196  pythagtrip  13200  pc1  13221  prmlem0  13420  acsfn0  13877  mgpress  15651  abvneg  15914  leordtval2  17268  txswaphmeo  17829  iccntr  18844  dvlipcn  19870  sinq34lt0t  20409  cosordlem  20425  efif1olem3  20438  basellem3  20857  ppiub  20980  bposlem9  21068  lgsne0  21109  lgsdinn0  21116  chebbnd1  21158  trls  21528  constr1trl  21580  constr2wlk  21590  constr2trl  21591  usgrcyclnl2  21620  4cycl4dv  21646  eupath2lem3  21693  mayete3i  23222  mayete3iOLD  23223  lnop0  23461  nmcexi  23521  nmoptrii  23589  nmopcoadji  23596  hstle1  23721  hst0  23728  strlem5  23750  jplem1  23763  lgamgulmlem2  24806  subfacp1lem5  24862  wfisg  25476  frinsg  25512  limsucncmpi  26187  fdc  26440  eldioph3b  26814  2spontn0vne  28307  sinhpcosh  28420
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 178  df-an 361
  Copyright terms: Public domain W3C validator