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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mpand  693  mpan2i  695  ralxfrd  5408  ralxfrd2  5412  sotri3  6137  predtrss  6330  oeordi  8608  coflton  8692  cofon1  8693  cofon2  8694  xpfiOLD  9344  ttrclss  9745  alephle  10113  axdc3lem4  10478  dedekindle  11410  addlsub  11662  letrp1  12091  ledivp1  12149  peano2uz2  12683  uzind  12687  xrre  13183  xrre2  13184  xrltmin  13196  xrlemin  13198  lemaxle  13209  xralrple  13219  xlemul1a  13302  xrinfmsslem  13322  flge  13806  flflp1  13808  fsequb  13976  seqcl2  14021  monoord  14033  facwordi  14284  facavg  14296  01sqrexlem6  15230  leabs  15282  caubnd  15341  limsupgre  15461  limsupbnd2  15463  lo1bdd2  15504  lo1bddrp  15505  o1lo1  15517  o1rlimmul  15599  lo1mul  15608  isercolllem2  15648  climcndslem1  15831  climcndslem2  15832  ruclem3  16213  ruclem9  16218  ruclem12  16221  dvdsmultr1  16276  ltoddhalfle  16341  divalglem0  16373  dvdsgcdb  16524  dfgcd2  16525  coprmgcdb  16623  coprmdvds2  16628  exprmfct  16678  prmdvdsfz  16679  prmfac1  16695  rpexp  16697  eulerthlem2  16754  pcpremul  16815  pcdvdsb  16841  pcprmpw2  16854  pockthlem  16877  prmreclem3  16890  4sqlem11  16927  vdwnnlem3  16969  meetle  18395  latjlej1  18448  latnlej2  18454  clatleglb  18513  mndodconglem  19508  efgsrel  19701  ablfac1b  20039  pgpfac1lem1  20043  lbsextlem2  21059  psdmul  22113  chfacfscmul0  22804  chfacfpmmul0  22808  lmcls  23250  ufileu  23867  ufilcmp  23980  cnpfcf  23989  tsmsxp  24103  prdsbl  24444  reconnlem2  24787  evth  24929  ivthlem2  25425  ivthlem3  25426  ovollb2lem  25461  ovoliunlem2  25476  ovolicc2lem3  25492  ismbf3d  25627  itg2seq  25716  itg2monolem1  25724  dvcnvrelem1  25994  itgsubst  26028  plypf1  26191  coeaddlem  26228  coemullem  26229  ulmcau  26376  abelth  26423  wilth  27048  ftalem2  27051  ftalem3  27052  muval1  27110  dvdssqf  27115  sqff1o  27159  chtub  27190  bposlem3  27264  lgsne0  27313  gausslemma2dlem1a  27343  gausslemma2dlem2  27345  lgseisenlem1  27353  lgseisenlem2  27354  lgsquadlem1  27358  lgsquadlem2  27359  lgsquadlem3  27360  lgsquad2lem1  27362  lgsquad2lem2  27363  dchrisum0lem1  27494  pntlem3  27587  negsbdaylem  28014  mulsproplem5  28070  mulsproplem8  28073  upgrewlkle2  29492  pthdlem1  29652  crctcshwlkn0lem3  29695  ex-natded5.8-2  30296  nmoub3i  30655  ubthlem1  30752  ubthlem2  30753  shsel1  31203  nmopub2tALT  31791  nmfnleub2  31808  lnconi  31915  eulerpartlemb  34119  dfon2lem4  35513  btwncomim  35740  nn0prpwlem  35937  ltflcei  37212  poimirlem9  37233  poimirlem18  37242  poimirlem21  37245  poimirlem22  37246  poimirlem24  37248  poimirlem29  37253  heicant  37259  mbfresfi  37270  itg2addnclem2  37276  itg2addnclem3  37277  incsequz  37352  heibor1lem  37413  atlelt  39041  1cvratex  39076  dalem3  39267  linepsubN  39355  pmapsub  39371  2llnma3r  39391  cdlemblem  39396  pmapjoin  39455  atmod1i1  39460  atmod1i2  39462  llnmod1i2  39463  lhpmcvr4N  39629  4atexlemnclw  39673  cdlemd3  39803  cdleme3g  39837  cdleme3h  39838  cdleme7d  39849  cdleme7ga  39851  cdleme21c  39930  cdleme35fnpq  40052  cdleme35f  40057  cdlemf1  40164  cdlemg4  40220  cdlemg6c  40223  cdlemg27a  40295  cdlemg33b0  40304  cdlemg33a  40309  cdlemk3  40436  dia2dimlem1  40667  dvheveccl  40715  dihord6apre  40859  dihord6b  40863  coprmdvdsb  42548  harval3  43110  monoordxrv  45002  stoweid  45589  smonoord  46848  iccpartgt  46904  goldbachthlem2  47023  lighneallem2  47083  tgoldbach  47294  nn0sumltlt  47600  dignn0flhalflem1  47874