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

Theorem mpan2d 655
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 425 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
41, 3mpid 37 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpand  656  mpan2i  658  ralxfrd  4564  sotri3  5089  oeordi  6601  xpfi  7144  alephle  7731  axdc3lem4  8095  letrp1  9614  ledivp1  9674  peano2uz2  10115  uzind  10119  xrre  10514  xrre2  10515  xrltmin  10527  xrlemin  10529  xralrple  10548  xlemul1a  10624  xrinfmsslem  10642  flge  10953  fsequb  11053  seqcl2  11080  monoord  11092  facwordi  11318  facavg  11330  sqrlem6  11749  leabs  11800  caubnd  11858  limsupgre  11971  limsupbnd2  11973  lo1bdd2  12014  lo1bddrp  12015  o1lo1  12027  o1rlimmul  12108  lo1mul  12117  isercolllem2  12155  climcndslem1  12324  climcndslem2  12325  ruclem3  12527  ruclem9  12532  ruclem12  12535  dvdsmultr1  12579  divalglem0  12608  dvdsgcdb  12739  coprmdvds2  12798  exprmfct  12805  prmfac1  12813  rpexp  12815  eulerthlem2  12866  pcpremul  12912  pcdvdsb  12937  pcprmpw2  12950  pockthlem  12968  prmreclem3  12981  4sqlem11  13018  vdwnnlem3  13060  meetle  14150  latjlej1  14187  latnlej2  14193  clatleglb  14246  mndodconglem  14872  efgsrel  15059  ablfac1b  15321  pgpfac1lem1  15325  lbsextlem2  15928  lmcls  17046  ufileu  17630  ufilcmp  17743  cnpfcf  17752  tsmsxp  17853  prdsbl  18053  reconnlem2  18348  evth  18473  ivthlem2  18828  ivthlem3  18829  ovollb2lem  18863  ovoliunlem2  18878  ovolicc2lem3  18894  ismbf3d  19025  itg2seq  19113  itg2monolem1  19121  dvcnvrelem1  19380  itgsubst  19412  plypf1  19610  coeaddlem  19646  coemullem  19647  ulmcau  19788  abelth  19833  wilth  20325  ftalem2  20327  ftalem3  20328  muval1  20387  dvdssqf  20392  sqff1o  20436  chtub  20467  bposlem3  20541  lgsne0  20588  lgseisenlem1  20604  lgseisenlem2  20605  lgsquadlem1  20609  lgsquadlem2  20610  lgsquadlem3  20611  lgsquad2lem1  20613  lgsquad2lem2  20614  dchrisum0lem1  20681  pntlem3  20774  ex-natded5.8-2  20817  nmoub3i  21367  ubthlem1  21465  ubthlem2  21466  shsel1  21916  nmopub2tALT  22505  nmfnleub2  22522  lnconi  22629  dedekindle  24098  dfon2lem4  24213  btwncomim  24708  ltflcei  24998  lxflflp1  25000  itg2addnclem2  25004  itg2addnc  25005  prltub  25363  nn0prpwlem  26341  incsequz  26561  heibor1lem  26636  coprmdvdsb  27177  stoweid  27915  atlelt  30249  1cvratex  30284  dalem3  30475  linepsubN  30563  pmapsub  30579  2llnma3r  30599  cdlemblem  30604  pmapjoin  30663  atmod1i1  30668  atmod1i2  30670  llnmod1i2  30671  lhpmcvr4N  30837  4atexlemnclw  30881  cdlemd3  31011  cdleme3g  31045  cdleme3h  31046  cdleme7d  31057  cdleme7ga  31059  cdleme21c  31138  cdleme35fnpq  31260  cdleme35f  31265  cdlemf1  31372  cdlemg4  31428  cdlemg6c  31431  cdlemg27a  31503  cdlemg33b0  31512  cdlemg33a  31517  cdlemk3  31644  dia2dimlem1  31876  dvheveccl  31924  dihord6apre  32068  dihord6b  32072
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