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  4730  sotri3  5257  oeordi  6823  xpfi  7371  alephle  7962  axdc3lem4  8326  letrp1  9845  ledivp1  9905  peano2uz2  10350  uzind  10354  xrre  10750  xrre2  10751  xrltmin  10763  xrlemin  10765  xralrple  10784  xlemul1a  10860  xrinfmsslem  10879  flge  11207  fsequb  11307  seqcl2  11334  monoord  11346  facwordi  11573  facavg  11585  sqrlem6  12046  leabs  12097  caubnd  12155  limsupgre  12268  limsupbnd2  12270  lo1bdd2  12311  lo1bddrp  12312  o1lo1  12324  o1rlimmul  12405  lo1mul  12414  isercolllem2  12452  climcndslem1  12622  climcndslem2  12623  ruclem3  12825  ruclem9  12830  ruclem12  12833  dvdsmultr1  12877  divalglem0  12906  dvdsgcdb  13037  coprmdvds2  13096  exprmfct  13103  prmfac1  13111  rpexp  13113  eulerthlem2  13164  pcpremul  13210  pcdvdsb  13235  pcprmpw2  13248  pockthlem  13266  prmreclem3  13279  4sqlem11  13316  vdwnnlem3  13358  meetle  14450  latjlej1  14487  latnlej2  14493  clatleglb  14546  mndodconglem  15172  efgsrel  15359  ablfac1b  15621  pgpfac1lem1  15625  lbsextlem2  16224  lmcls  17359  ufileu  17944  ufilcmp  18057  cnpfcf  18066  tsmsxp  18177  prdsbl  18514  reconnlem2  18851  evth  18977  ivthlem2  19342  ivthlem3  19343  ovollb2lem  19377  ovoliunlem2  19392  ovolicc2lem3  19408  ismbf3d  19539  itg2seq  19627  itg2monolem1  19635  dvcnvrelem1  19894  itgsubst  19926  plypf1  20124  coeaddlem  20160  coemullem  20161  ulmcau  20304  abelth  20350  wilth  20847  ftalem2  20849  ftalem3  20850  muval1  20909  dvdssqf  20914  sqff1o  20958  chtub  20989  bposlem3  21063  lgsne0  21110  lgseisenlem1  21126  lgseisenlem2  21127  lgsquadlem1  21131  lgsquadlem2  21132  lgsquadlem3  21133  lgsquad2lem1  21135  lgsquad2lem2  21136  dchrisum0lem1  21203  pntlem3  21296  nmoub3i  22267  ubthlem1  22365  ubthlem2  22366  shsel1  22816  nmopub2tALT  23405  nmfnleub2  23422  lnconi  23529  dedekindle  25181  dfon2lem4  25406  btwncomim  25940  ltflcei  26232  lxflflp1  26234  mbfresfi  26244  itg2addnclem2  26248  itg2addnclem3  26249  nn0prpwlem  26317  incsequz  26444  heibor1lem  26510  coprmdvdsb  27044  stoweid  27780  ralxfrd2  28060  atlelt  30173  1cvratex  30208  dalem3  30399  linepsubN  30487  pmapsub  30503  2llnma3r  30523  cdlemblem  30528  pmapjoin  30587  atmod1i1  30592  atmod1i2  30594  llnmod1i2  30595  lhpmcvr4N  30761  4atexlemnclw  30805  cdlemd3  30935  cdleme3g  30969  cdleme3h  30970  cdleme7d  30981  cdleme7ga  30983  cdleme21c  31062  cdleme35fnpq  31184  cdleme35f  31189  cdlemf1  31296  cdlemg4  31352  cdlemg6c  31355  cdlemg27a  31427  cdlemg33b0  31436  cdlemg33a  31441  cdlemk3  31568  dia2dimlem1  31800  dvheveccl  31848  dihord6apre  31992  dihord6b  31996
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