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  4677  sotri3  5204  oeordi  6766  xpfi  7314  alephle  7902  axdc3lem4  8266  letrp1  9784  ledivp1  9844  peano2uz2  10289  uzind  10293  xrre  10689  xrre2  10690  xrltmin  10702  xrlemin  10704  xralrple  10723  xlemul1a  10799  xrinfmsslem  10818  flge  11141  fsequb  11241  seqcl2  11268  monoord  11280  facwordi  11507  facavg  11519  sqrlem6  11980  leabs  12031  caubnd  12089  limsupgre  12202  limsupbnd2  12204  lo1bdd2  12245  lo1bddrp  12246  o1lo1  12258  o1rlimmul  12339  lo1mul  12348  isercolllem2  12386  climcndslem1  12556  climcndslem2  12557  ruclem3  12759  ruclem9  12764  ruclem12  12767  dvdsmultr1  12811  divalglem0  12840  dvdsgcdb  12971  coprmdvds2  13030  exprmfct  13037  prmfac1  13045  rpexp  13047  eulerthlem2  13098  pcpremul  13144  pcdvdsb  13169  pcprmpw2  13182  pockthlem  13200  prmreclem3  13213  4sqlem11  13250  vdwnnlem3  13292  meetle  14384  latjlej1  14421  latnlej2  14427  clatleglb  14480  mndodconglem  15106  efgsrel  15293  ablfac1b  15555  pgpfac1lem1  15559  lbsextlem2  16158  lmcls  17288  ufileu  17872  ufilcmp  17985  cnpfcf  17994  tsmsxp  18105  prdsbl  18411  reconnlem2  18729  evth  18855  ivthlem2  19216  ivthlem3  19217  ovollb2lem  19251  ovoliunlem2  19266  ovolicc2lem3  19282  ismbf3d  19413  itg2seq  19501  itg2monolem1  19509  dvcnvrelem1  19768  itgsubst  19800  plypf1  19998  coeaddlem  20034  coemullem  20035  ulmcau  20178  abelth  20224  wilth  20721  ftalem2  20723  ftalem3  20724  muval1  20783  dvdssqf  20788  sqff1o  20832  chtub  20863  bposlem3  20937  lgsne0  20984  lgseisenlem1  21000  lgseisenlem2  21001  lgsquadlem1  21005  lgsquadlem2  21006  lgsquadlem3  21007  lgsquad2lem1  21009  lgsquad2lem2  21010  dchrisum0lem1  21077  pntlem3  21170  nmoub3i  22122  ubthlem1  22220  ubthlem2  22221  shsel1  22671  nmopub2tALT  23260  nmfnleub2  23277  lnconi  23384  dedekindle  24967  dfon2lem4  25166  btwncomim  25661  ltflcei  25950  lxflflp1  25952  itg2addnclem2  25958  itg2addnc  25959  nn0prpwlem  26016  incsequz  26143  heibor1lem  26209  coprmdvdsb  26743  stoweid  27480  atlelt  29552  1cvratex  29587  dalem3  29778  linepsubN  29866  pmapsub  29882  2llnma3r  29902  cdlemblem  29907  pmapjoin  29966  atmod1i1  29971  atmod1i2  29973  llnmod1i2  29974  lhpmcvr4N  30140  4atexlemnclw  30184  cdlemd3  30314  cdleme3g  30348  cdleme3h  30349  cdleme7d  30360  cdleme7ga  30362  cdleme21c  30441  cdleme35fnpq  30563  cdleme35f  30568  cdlemf1  30675  cdlemg4  30731  cdlemg6c  30734  cdlemg27a  30806  cdlemg33b0  30815  cdlemg33a  30820  cdlemk3  30947  dia2dimlem1  31179  dvheveccl  31227  dihord6apre  31371  dihord6b  31375
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