Theorem mpan2d 692

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mpan2d.1	⊢ (𝜑 → 𝜒)
mpan2d.2	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mpan2d	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem mpan2d

Step	Hyp	Ref	Expression
1		mpan2d.1	. 2 ⊢ (𝜑 → 𝜒)
2		mpan2d.2	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 418	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpid 44	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpand  693  mpan2i  695  ralxfrd  5312  ralxfrd2  5316  sotri3  5993  oeordi  8216  xpfi  8792  alephle  9517  axdc3lem4  9878  dedekindle  10807  addlsub  11059  letrp1  11487  ledivp1  11545  peano2uz2  12073  uzind  12077  xrre  12565  xrre2  12566  xrltmin  12578  xrlemin  12580  lemaxle  12591  xralrple  12601  xlemul1a  12684  xrinfmsslem  12704  flge  13178  flflp1  13180  fsequb  13346  seqcl2  13391  monoord  13403  facwordi  13652  facavg  13664  sqrlem6  14610  leabs  14662  caubnd  14721  limsupgre  14841  limsupbnd2  14843  lo1bdd2  14884  lo1bddrp  14885  o1lo1  14897  o1rlimmul  14978  lo1mul  14987  isercolllem2  15025  climcndslem1  15207  climcndslem2  15208  ruclem3  15589  ruclem9  15594  ruclem12  15597  dvdsmultr1  15650  ltoddhalfle  15713  divalglem0  15747  dvdsgcdb  15896  dfgcd2  15897  coprmgcdb  15996  coprmdvds2  16001  exprmfct  16051  prmdvdsfz  16052  prmfac1  16066  rpexp  16067  eulerthlem2  16122  pcpremul  16183  pcdvdsb  16208  pcprmpw2  16221  pockthlem  16244  prmreclem3  16257  4sqlem11  16294  vdwnnlem3  16336  meetle  17641  latjlej1  17678  latnlej2  17684  clatleglb  17739  mndodconglem  18672  efgsrel  18863  ablfac1b  19195  pgpfac1lem1  19199  lbsextlem2  19934  chfacfscmul0  21469  chfacfpmmul0  21473  lmcls  21913  ufileu  22530  ufilcmp  22643  cnpfcf  22652  tsmsxp  22766  prdsbl  23104  reconnlem2  23438  evth  23566  ivthlem2  24056  ivthlem3  24057  ovollb2lem  24092  ovoliunlem2  24107  ovolicc2lem3  24123  ismbf3d  24258  itg2seq  24346  itg2monolem1  24354  dvcnvrelem1  24617  itgsubst  24649  plypf1  24805  coeaddlem  24842  coemullem  24843  ulmcau  24986  abelth  25032  wilth  25651  ftalem2  25654  ftalem3  25655  muval1  25713  dvdssqf  25718  sqff1o  25762  chtub  25791  bposlem3  25865  lgsne0  25914  gausslemma2dlem1a  25944  gausslemma2dlem2  25946  lgseisenlem1  25954  lgseisenlem2  25955  lgsquadlem1  25959  lgsquadlem2  25960  lgsquadlem3  25961  lgsquad2lem1  25963  lgsquad2lem2  25964  dchrisum0lem1  26095  pntlem3  26188  upgrewlkle2  27391  pthdlem1  27550  crctcshwlkn0lem3  27593  ex-natded5.8-2  28196  nmoub3i  28553  ubthlem1  28650  ubthlem2  28651  shsel1  29101  nmopub2tALT  29689  nmfnleub2  29706  lnconi  29813  eulerpartlemb  31630  dfon2lem4  33035  btwncomim  33478  nn0prpwlem  33674  ltflcei  34884  poimirlem9  34905  poimirlem18  34914  poimirlem21  34917  poimirlem22  34918  poimirlem24  34920  poimirlem29  34925  heicant  34931  mbfresfi  34942  itg2addnclem2  34948  itg2addnclem3  34949  incsequz  35027  heibor1lem  35091  atlelt  36578  1cvratex  36613  dalem3  36804  linepsubN  36892  pmapsub  36908  2llnma3r  36928  cdlemblem  36933  pmapjoin  36992  atmod1i1  36997  atmod1i2  36999  llnmod1i2  37000  lhpmcvr4N  37166  4atexlemnclw  37210  cdlemd3  37340  cdleme3g  37374  cdleme3h  37375  cdleme7d  37386  cdleme7ga  37388  cdleme21c  37467  cdleme35fnpq  37589  cdleme35f  37594  cdlemf1  37701  cdlemg4  37757  cdlemg6c  37760  cdlemg27a  37832  cdlemg33b0  37841  cdlemg33a  37846  cdlemk3  37973  dia2dimlem1  38204  dvheveccl  38252  dihord6apre  38396  dihord6b  38400  coprmdvdsb  39588  harval3  39910  monoordxrv  41764  stoweid  42355  smonoord  43538  iccpartgt  43594  goldbachthlem2  43715  lighneallem2  43778  tgoldbach  43989  nn0sumltlt  44405  dignn0flhalflem1  44682