Theorem mpan2d 710

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

Step	Hyp	Ref	Expression
1		mpan2d.1	. 2 |- ( ph -> ch )
2		mpan2d.2	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
3	2	expd 452	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
4	1, 3	mpid 44	1 |- ( ph -> ( ps -> th ) )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  mpand  711  mpan2i  713  ralxfrd  4879  ralxfrdOLD  4880  ralxfrd2  4884  sotri3  5526  oeordi  7667  xpfi  8231  alephle  8911  axdc3lem4  9275  dedekindle  10201  addlsub  10447  letrp1  10865  ledivp1  10925  peano2uz2  11465  uzind  11469  xrre  12000  xrre2  12001  xrltmin  12013  xrlemin  12015  lemaxle  12026  xralrple  12036  xlemul1a  12118  xrinfmsslem  12138  flge  12606  flflp1  12608  fsequb  12774  seqcl2  12819  monoord  12831  facwordi  13076  facavg  13088  sqrlem6  13988  leabs  14039  caubnd  14098  limsupgre  14212  limsupbnd2  14214  lo1bdd2  14255  lo1bddrp  14256  o1lo1  14268  o1rlimmul  14349  lo1mul  14358  isercolllem2  14396  climcndslem1  14581  climcndslem2  14582  ruclem3  14962  ruclem9  14967  ruclem12  14970  dvdsmultr1  15019  ltoddhalfle  15085  divalglem0  15116  dvdsgcdb  15262  dfgcd2  15263  coprmgcdb  15362  coprmdvds2  15368  exprmfct  15416  prmdvdsfz  15417  prmfac1  15431  rpexp  15432  eulerthlem2  15487  pcpremul  15548  pcdvdsb  15573  pcprmpw2  15586  pockthlem  15609  prmreclem3  15622  4sqlem11  15659  vdwnnlem3  15701  meetle  17028  latjlej1  17065  latnlej2  17071  clatleglb  17126  mndodconglem  17960  efgsrel  18147  ablfac1b  18469  pgpfac1lem1  18473  lbsextlem2  19159  chfacfscmul0  20663  chfacfpmmul0  20667  lmcls  21106  ufileu  21723  ufilcmp  21836  cnpfcf  21845  tsmsxp  21958  prdsbl  22296  reconnlem2  22630  evth  22758  ivthlem2  23221  ivthlem3  23222  ovollb2lem  23256  ovoliunlem2  23271  ovolicc2lem3  23287  ismbf3d  23421  itg2seq  23509  itg2monolem1  23517  dvcnvrelem1  23780  itgsubst  23812  plypf1  23968  coeaddlem  24005  coemullem  24006  ulmcau  24149  abelth  24195  wilth  24797  ftalem2  24800  ftalem3  24801  muval1  24859  dvdssqf  24864  sqff1o  24908  chtub  24937  bposlem3  25011  lgsne0  25060  gausslemma2dlem1a  25090  gausslemma2dlem2  25092  lgseisenlem1  25100  lgseisenlem2  25101  lgsquadlem1  25105  lgsquadlem2  25106  lgsquadlem3  25107  lgsquad2lem1  25109  lgsquad2lem2  25110  dchrisum0lem1  25205  pntlem3  25298  upgrewlkle2  26502  pthdlem1  26662  crctcshwlkn0lem3  26704  ex-natded5.8-2  27271  nmoub3i  27628  ubthlem1  27726  ubthlem2  27727  shsel1  28180  nmopub2tALT  28768  nmfnleub2  28785  lnconi  28892  eulerpartlemb  30430  dfon2lem4  31691  btwncomim  32120  nn0prpwlem  32317  ltflcei  33397  poimirlem9  33418  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem24  33433  poimirlem29  33438  heicant  33444  mbfresfi  33456  itg2addnclem2  33462  itg2addnclem3  33463  incsequz  33544  heibor1lem  33608  atlelt  34724  1cvratex  34759  dalem3  34950  linepsubN  35038  pmapsub  35054  2llnma3r  35074  cdlemblem  35079  pmapjoin  35138  atmod1i1  35143  atmod1i2  35145  llnmod1i2  35146  lhpmcvr4N  35312  4atexlemnclw  35356  cdlemd3  35487  cdleme3g  35521  cdleme3h  35522  cdleme7d  35533  cdleme7ga  35535  cdleme21c  35615  cdleme35fnpq  35737  cdleme35f  35742  cdlemf1  35849  cdlemg4  35905  cdlemg6c  35908  cdlemg27a  35980  cdlemg33b0  35989  cdlemg33a  35994  cdlemk3  36121  dia2dimlem1  36353  dvheveccl  36401  dihord6apre  36545  dihord6b  36549  coprmdvdsb  37552  stoweid  40280  smonoord  41341  iccpartgt  41363  goldbachthlem2  41458  lighneallem2  41523  tgoldbach  41705  tgoldbachOLD  41712  nn0sumltlt  42128  dignn0flhalflem1  42409