MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpan2d Structured version   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  4737  sotri3  5264  oeordi  6830  xpfi  7378  alephle  7969  axdc3lem4  8333  letrp1  9852  ledivp1  9912  peano2uz2  10357  uzind  10361  xrre  10757  xrre2  10758  xrltmin  10770  xrlemin  10772  xralrple  10791  xlemul1a  10867  xrinfmsslem  10886  flge  11214  fsequb  11314  seqcl2  11341  monoord  11353  facwordi  11580  facavg  11592  sqrlem6  12053  leabs  12104  caubnd  12162  limsupgre  12275  limsupbnd2  12277  lo1bdd2  12318  lo1bddrp  12319  o1lo1  12331  o1rlimmul  12412  lo1mul  12421  isercolllem2  12459  climcndslem1  12629  climcndslem2  12630  ruclem3  12832  ruclem9  12837  ruclem12  12840  dvdsmultr1  12884  divalglem0  12913  dvdsgcdb  13044  coprmdvds2  13103  exprmfct  13110  prmfac1  13118  rpexp  13120  eulerthlem2  13171  pcpremul  13217  pcdvdsb  13242  pcprmpw2  13255  pockthlem  13273  prmreclem3  13286  4sqlem11  13323  vdwnnlem3  13365  meetle  14457  latjlej1  14494  latnlej2  14500  clatleglb  14553  mndodconglem  15179  efgsrel  15366  ablfac1b  15628  pgpfac1lem1  15632  lbsextlem2  16231  lmcls  17366  ufileu  17951  ufilcmp  18064  cnpfcf  18073  tsmsxp  18184  prdsbl  18521  reconnlem2  18858  evth  18984  ivthlem2  19349  ivthlem3  19350  ovollb2lem  19384  ovoliunlem2  19399  ovolicc2lem3  19415  ismbf3d  19546  itg2seq  19634  itg2monolem1  19642  dvcnvrelem1  19901  itgsubst  19933  plypf1  20131  coeaddlem  20167  coemullem  20168  ulmcau  20311  abelth  20357  wilth  20854  ftalem2  20856  ftalem3  20857  muval1  20916  dvdssqf  20921  sqff1o  20965  chtub  20996  bposlem3  21070  lgsne0  21117  lgseisenlem1  21133  lgseisenlem2  21134  lgsquadlem1  21138  lgsquadlem2  21139  lgsquadlem3  21140  lgsquad2lem1  21142  lgsquad2lem2  21143  dchrisum0lem1  21210  pntlem3  21303  nmoub3i  22274  ubthlem1  22372  ubthlem2  22373  shsel1  22823  nmopub2tALT  23412  nmfnleub2  23429  lnconi  23536  dedekindle  25188  dfon2lem4  25413  btwncomim  25947  ltflcei  26239  lxflflp1  26241  mbfresfi  26253  itg2addnclem2  26257  itg2addnclem3  26258  nn0prpwlem  26325  incsequz  26452  heibor1lem  26518  coprmdvdsb  27052  stoweid  27788  ralxfrd2  28072  atlelt  30235  1cvratex  30270  dalem3  30461  linepsubN  30549  pmapsub  30565  2llnma3r  30585  cdlemblem  30590  pmapjoin  30649  atmod1i1  30654  atmod1i2  30656  llnmod1i2  30657  lhpmcvr4N  30823  4atexlemnclw  30867  cdlemd3  30997  cdleme3g  31031  cdleme3h  31032  cdleme7d  31043  cdleme7ga  31045  cdleme21c  31124  cdleme35fnpq  31246  cdleme35f  31251  cdlemf1  31358  cdlemg4  31414  cdlemg6c  31417  cdlemg27a  31489  cdlemg33b0  31498  cdlemg33a  31503  cdlemk3  31630  dia2dimlem1  31862  dvheveccl  31910  dihord6apre  32054  dihord6b  32058
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