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

Theorem mpan2d 656
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mpan2d.1  |-  ( ph  ->  ch )
mpan2d.2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mpan2d  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem mpan2d
StepHypRef Expression
1 mpan2d.1 . 2  |-  ( ph  ->  ch )
2 mpan2d.2 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
32exp3a 426 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
41, 3mpid 39 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpand  657  mpan2i  659  ralxfrd  4696  sotri3  5223  oeordi  6789  xpfi  7337  alephle  7925  axdc3lem4  8289  letrp1  9808  ledivp1  9868  peano2uz2  10313  uzind  10317  xrre  10713  xrre2  10714  xrltmin  10726  xrlemin  10728  xralrple  10747  xlemul1a  10823  xrinfmsslem  10842  flge  11169  fsequb  11269  seqcl2  11296  monoord  11308  facwordi  11535  facavg  11547  sqrlem6  12008  leabs  12059  caubnd  12117  limsupgre  12230  limsupbnd2  12232  lo1bdd2  12273  lo1bddrp  12274  o1lo1  12286  o1rlimmul  12367  lo1mul  12376  isercolllem2  12414  climcndslem1  12584  climcndslem2  12585  ruclem3  12787  ruclem9  12792  ruclem12  12795  dvdsmultr1  12839  divalglem0  12868  dvdsgcdb  12999  coprmdvds2  13058  exprmfct  13065  prmfac1  13073  rpexp  13075  eulerthlem2  13126  pcpremul  13172  pcdvdsb  13197  pcprmpw2  13210  pockthlem  13228  prmreclem3  13241  4sqlem11  13278  vdwnnlem3  13320  meetle  14412  latjlej1  14449  latnlej2  14455  clatleglb  14508  mndodconglem  15134  efgsrel  15321  ablfac1b  15583  pgpfac1lem1  15587  lbsextlem2  16186  lmcls  17320  ufileu  17904  ufilcmp  18017  cnpfcf  18026  tsmsxp  18137  prdsbl  18474  reconnlem2  18811  evth  18937  ivthlem2  19302  ivthlem3  19303  ovollb2lem  19337  ovoliunlem2  19352  ovolicc2lem3  19368  ismbf3d  19499  itg2seq  19587  itg2monolem1  19595  dvcnvrelem1  19854  itgsubst  19886  plypf1  20084  coeaddlem  20120  coemullem  20121  ulmcau  20264  abelth  20310  wilth  20807  ftalem2  20809  ftalem3  20810  muval1  20869  dvdssqf  20874  sqff1o  20918  chtub  20949  bposlem3  21023  lgsne0  21070  lgseisenlem1  21086  lgseisenlem2  21087  lgsquadlem1  21091  lgsquadlem2  21092  lgsquadlem3  21093  lgsquad2lem1  21095  lgsquad2lem2  21096  dchrisum0lem1  21163  pntlem3  21256  nmoub3i  22227  ubthlem1  22325  ubthlem2  22326  shsel1  22776  nmopub2tALT  23365  nmfnleub2  23382  lnconi  23489  dedekindle  25141  dfon2lem4  25356  btwncomim  25851  ltflcei  26140  lxflflp1  26142  mbfresfi  26152  itg2addnclem2  26156  itg2addnclem3  26157  nn0prpwlem  26215  incsequz  26342  heibor1lem  26408  coprmdvdsb  26942  stoweid  27679  atlelt  29920  1cvratex  29955  dalem3  30146  linepsubN  30234  pmapsub  30250  2llnma3r  30270  cdlemblem  30275  pmapjoin  30334  atmod1i1  30339  atmod1i2  30341  llnmod1i2  30342  lhpmcvr4N  30508  4atexlemnclw  30552  cdlemd3  30682  cdleme3g  30716  cdleme3h  30717  cdleme7d  30728  cdleme7ga  30730  cdleme21c  30809  cdleme35fnpq  30931  cdleme35f  30936  cdlemf1  31043  cdlemg4  31099  cdlemg6c  31102  cdlemg27a  31174  cdlemg33b0  31183  cdlemg33a  31188  cdlemk3  31315  dia2dimlem1  31547  dvheveccl  31595  dihord6apre  31739  dihord6b  31743
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