Theorem mpan2d 681

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 408	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpid 44	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  mpand  682  mpan2i  684  ralxfrd  5156  ralxfrd2  5160  sotri3  5824  oeordi  8006  xpfi  8576  alephle  9300  axdc3lem4  9665  dedekindle  10596  addlsub  10849  letrp1  11277  ledivp1  11335  peano2uz2  11876  uzind  11880  xrre  12372  xrre2  12373  xrltmin  12385  xrlemin  12387  lemaxle  12398  xralrple  12408  xlemul1a  12490  xrinfmsslem  12510  flge  12983  flflp1  12985  fsequb  13151  seqcl2  13196  monoord  13208  facwordi  13457  facavg  13469  sqrlem6  14458  leabs  14510  caubnd  14569  limsupgre  14689  limsupbnd2  14691  lo1bdd2  14732  lo1bddrp  14733  o1lo1  14745  o1rlimmul  14826  lo1mul  14835  isercolllem2  14873  climcndslem1  15054  climcndslem2  15055  ruclem3  15436  ruclem9  15441  ruclem12  15444  dvdsmultr1  15497  ltoddhalfle  15560  divalglem0  15594  dvdsgcdb  15739  dfgcd2  15740  coprmgcdb  15839  coprmdvds2  15844  exprmfct  15894  prmdvdsfz  15895  prmfac1  15909  rpexp  15910  eulerthlem2  15965  pcpremul  16026  pcdvdsb  16051  pcprmpw2  16064  pockthlem  16087  prmreclem3  16100  4sqlem11  16137  vdwnnlem3  16179  meetle  17486  latjlej1  17523  latnlej2  17529  clatleglb  17584  mndodconglem  18421  efgsrel  18608  ablfac1b  18932  pgpfac1lem1  18936  lbsextlem2  19643  chfacfscmul0  21160  chfacfpmmul0  21164  lmcls  21604  ufileu  22221  ufilcmp  22334  cnpfcf  22343  tsmsxp  22456  prdsbl  22794  reconnlem2  23128  evth  23256  ivthlem2  23746  ivthlem3  23747  ovollb2lem  23782  ovoliunlem2  23797  ovolicc2lem3  23813  ismbf3d  23948  itg2seq  24036  itg2monolem1  24044  dvcnvrelem1  24307  itgsubst  24339  plypf1  24495  coeaddlem  24532  coemullem  24533  ulmcau  24676  abelth  24722  wilth  25340  ftalem2  25343  ftalem3  25344  muval1  25402  dvdssqf  25407  sqff1o  25451  chtub  25480  bposlem3  25554  lgsne0  25603  gausslemma2dlem1a  25633  gausslemma2dlem2  25635  lgseisenlem1  25643  lgseisenlem2  25644  lgsquadlem1  25648  lgsquadlem2  25649  lgsquadlem3  25650  lgsquad2lem1  25652  lgsquad2lem2  25653  dchrisum0lem1  25784  pntlem3  25877  upgrewlkle2  27081  pthdlem1  27245  crctcshwlkn0lem3  27288  ex-natded5.8-2  27961  nmoub3i  28317  ubthlem1  28415  ubthlem2  28416  shsel1  28869  nmopub2tALT  29457  nmfnleub2  29474  lnconi  29581  eulerpartlemb  31228  dfon2lem4  32491  btwncomim  32935  nn0prpwlem  33131  ltflcei  34269  poimirlem9  34290  poimirlem18  34299  poimirlem21  34302  poimirlem22  34303  poimirlem24  34305  poimirlem29  34310  heicant  34316  mbfresfi  34327  itg2addnclem2  34333  itg2addnclem3  34334  incsequz  34413  heibor1lem  34477  atlelt  35967  1cvratex  36002  dalem3  36193  linepsubN  36281  pmapsub  36297  2llnma3r  36317  cdlemblem  36322  pmapjoin  36381  atmod1i1  36386  atmod1i2  36388  llnmod1i2  36389  lhpmcvr4N  36555  4atexlemnclw  36599  cdlemd3  36729  cdleme3g  36763  cdleme3h  36764  cdleme7d  36775  cdleme7ga  36777  cdleme21c  36856  cdleme35fnpq  36978  cdleme35f  36983  cdlemf1  37090  cdlemg4  37146  cdlemg6c  37149  cdlemg27a  37221  cdlemg33b0  37230  cdlemg33a  37235  cdlemk3  37362  dia2dimlem1  37593  dvheveccl  37641  dihord6apre  37785  dihord6b  37789  coprmdvdsb  38923  monoordxrv  41135  stoweid  41725  smonoord  42883  iccpartgt  42905  goldbachthlem2  43016  lighneallem2  43079  tgoldbach  43290  nn0sumltlt  43702  dignn0flhalflem1  43983