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  4548  sotri3  5073  oeordi  6585  xpfi  7128  alephle  7715  axdc3lem4  8079  letrp1  9598  ledivp1  9658  peano2uz2  10099  uzind  10103  xrre  10498  xrre2  10499  xrltmin  10511  xrlemin  10513  xralrple  10532  xlemul1a  10608  xrinfmsslem  10626  flge  10937  fsequb  11037  seqcl2  11064  monoord  11076  facwordi  11302  facavg  11314  sqrlem6  11733  leabs  11784  caubnd  11842  limsupgre  11955  limsupbnd2  11957  lo1bdd2  11998  lo1bddrp  11999  o1lo1  12011  o1rlimmul  12092  lo1mul  12101  isercolllem2  12139  climcndslem1  12308  climcndslem2  12309  ruclem3  12511  ruclem9  12516  ruclem12  12519  dvdsmultr1  12563  divalglem0  12592  dvdsgcdb  12723  coprmdvds2  12782  exprmfct  12789  prmfac1  12797  rpexp  12799  eulerthlem2  12850  pcpremul  12896  pcdvdsb  12921  pcprmpw2  12934  pockthlem  12952  prmreclem3  12965  4sqlem11  13002  vdwnnlem3  13044  meetle  14134  latjlej1  14171  latnlej2  14177  clatleglb  14230  mndodconglem  14856  efgsrel  15043  ablfac1b  15305  pgpfac1lem1  15309  lbsextlem2  15912  lmcls  17030  ufileu  17614  ufilcmp  17727  cnpfcf  17736  tsmsxp  17837  prdsbl  18037  reconnlem2  18332  evth  18457  ivthlem2  18812  ivthlem3  18813  ovollb2lem  18847  ovoliunlem2  18862  ovolicc2lem3  18878  ismbf3d  19009  itg2seq  19097  itg2monolem1  19105  dvcnvrelem1  19364  itgsubst  19396  plypf1  19594  coeaddlem  19630  coemullem  19631  ulmcau  19772  abelth  19817  wilth  20309  ftalem2  20311  ftalem3  20312  muval1  20371  dvdssqf  20376  sqff1o  20420  chtub  20451  bposlem3  20525  lgsne0  20572  lgseisenlem1  20588  lgseisenlem2  20589  lgsquadlem1  20593  lgsquadlem2  20594  lgsquadlem3  20595  lgsquad2lem1  20597  lgsquad2lem2  20598  dchrisum0lem1  20665  pntlem3  20758  ex-natded5.8-2  20801  nmoub3i  21351  ubthlem1  21449  ubthlem2  21450  shsel1  21900  nmopub2tALT  22489  nmfnleub2  22506  lnconi  22613  dedekindle  24083  dfon2lem4  24142  btwncomim  24636  prltub  25260  nn0prpwlem  26238  incsequz  26458  heibor1lem  26533  coprmdvdsb  27074  stoweid  27812  atlelt  29627  1cvratex  29662  dalem3  29853  linepsubN  29941  pmapsub  29957  2llnma3r  29977  cdlemblem  29982  pmapjoin  30041  atmod1i1  30046  atmod1i2  30048  llnmod1i2  30049  lhpmcvr4N  30215  4atexlemnclw  30259  cdlemd3  30389  cdleme3g  30423  cdleme3h  30424  cdleme7d  30435  cdleme7ga  30437  cdleme21c  30516  cdleme35fnpq  30638  cdleme35f  30643  cdlemf1  30750  cdlemg4  30806  cdlemg6c  30809  cdlemg27a  30881  cdlemg33b0  30890  cdlemg33a  30895  cdlemk3  31022  dia2dimlem1  31254  dvheveccl  31302  dihord6apre  31446  dihord6b  31450
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