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  5309  ralxfrd2  5313  sotri3  5990  oeordi  8213  xpfi  8789  alephle  9514  axdc3lem4  9875  dedekindle  10804  addlsub  11056  letrp1  11484  ledivp1  11542  peano2uz2  12071  uzind  12075  xrre  12563  xrre2  12564  xrltmin  12576  xrlemin  12578  lemaxle  12589  xralrple  12599  xlemul1a  12682  xrinfmsslem  12702  flge  13176  flflp1  13178  fsequb  13344  seqcl2  13389  monoord  13401  facwordi  13650  facavg  13662  sqrlem6  14607  leabs  14659  caubnd  14718  limsupgre  14838  limsupbnd2  14840  lo1bdd2  14881  lo1bddrp  14882  o1lo1  14894  o1rlimmul  14975  lo1mul  14984  isercolllem2  15022  climcndslem1  15204  climcndslem2  15205  ruclem3  15586  ruclem9  15591  ruclem12  15594  dvdsmultr1  15647  ltoddhalfle  15710  divalglem0  15744  dvdsgcdb  15893  dfgcd2  15894  coprmgcdb  15993  coprmdvds2  15998  exprmfct  16048  prmdvdsfz  16049  prmfac1  16063  rpexp  16064  eulerthlem2  16119  pcpremul  16180  pcdvdsb  16205  pcprmpw2  16218  pockthlem  16241  prmreclem3  16254  4sqlem11  16291  vdwnnlem3  16333  meetle  17638  latjlej1  17675  latnlej2  17681  clatleglb  17736  mndodconglem  18669  efgsrel  18860  ablfac1b  19192  pgpfac1lem1  19196  lbsextlem2  19931  chfacfscmul0  21466  chfacfpmmul0  21470  lmcls  21910  ufileu  22527  ufilcmp  22640  cnpfcf  22649  tsmsxp  22763  prdsbl  23101  reconnlem2  23435  evth  23563  ivthlem2  24053  ivthlem3  24054  ovollb2lem  24089  ovoliunlem2  24104  ovolicc2lem3  24120  ismbf3d  24255  itg2seq  24343  itg2monolem1  24351  dvcnvrelem1  24614  itgsubst  24646  plypf1  24802  coeaddlem  24839  coemullem  24840  ulmcau  24983  abelth  25029  wilth  25648  ftalem2  25651  ftalem3  25652  muval1  25710  dvdssqf  25715  sqff1o  25759  chtub  25788  bposlem3  25862  lgsne0  25911  gausslemma2dlem1a  25941  gausslemma2dlem2  25943  lgseisenlem1  25951  lgseisenlem2  25952  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  lgsquad2lem1  25960  lgsquad2lem2  25961  dchrisum0lem1  26092  pntlem3  26185  upgrewlkle2  27388  pthdlem1  27547  crctcshwlkn0lem3  27590  ex-natded5.8-2  28193  nmoub3i  28550  ubthlem1  28647  ubthlem2  28648  shsel1  29098  nmopub2tALT  29686  nmfnleub2  29703  lnconi  29810  eulerpartlemb  31626  dfon2lem4  33031  btwncomim  33474  nn0prpwlem  33670  ltflcei  34895  poimirlem9  34916  poimirlem18  34925  poimirlem21  34928  poimirlem22  34929  poimirlem24  34931  poimirlem29  34936  heicant  34942  mbfresfi  34953  itg2addnclem2  34959  itg2addnclem3  34960  incsequz  35038  heibor1lem  35102  atlelt  36589  1cvratex  36624  dalem3  36815  linepsubN  36903  pmapsub  36919  2llnma3r  36939  cdlemblem  36944  pmapjoin  37003  atmod1i1  37008  atmod1i2  37010  llnmod1i2  37011  lhpmcvr4N  37177  4atexlemnclw  37221  cdlemd3  37351  cdleme3g  37385  cdleme3h  37386  cdleme7d  37397  cdleme7ga  37399  cdleme21c  37478  cdleme35fnpq  37600  cdleme35f  37605  cdlemf1  37712  cdlemg4  37768  cdlemg6c  37771  cdlemg27a  37843  cdlemg33b0  37852  cdlemg33a  37857  cdlemk3  37984  dia2dimlem1  38215  dvheveccl  38263  dihord6apre  38407  dihord6b  38411  coprmdvdsb  39602  harval3  39924  monoordxrv  41778  stoweid  42368  smonoord  43551  iccpartgt  43607  goldbachthlem2  43728  lighneallem2  43791  tgoldbach  44002  nn0sumltlt  44418  dignn0flhalflem1  44695