Theorem mpan2d 694

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpand  695  mpan2i  697  ralxfrd  5353  ralxfrd2  5357  sotri3  6087  predtrss  6280  oeordi  8515  coflton  8599  cofon1  8600  cofon2  8601  ttrclss  9629  alephle  9998  axdc3lem4  10363  dedekindle  11297  addlsub  11553  letrp1  11985  ledivp1  12044  peano2uz2  12580  uzind  12584  xrre  13084  xrre2  13085  xrltmin  13097  xrlemin  13099  lemaxle  13110  xralrple  13120  xlemul1a  13203  xrinfmsslem  13223  flge  13725  flflp1  13727  fsequb  13898  seqcl2  13943  monoord  13955  facwordi  14212  facavg  14224  01sqrexlem6  15170  leabs  15222  caubnd  15282  limsupgre  15404  limsupbnd2  15406  lo1bdd2  15447  lo1bddrp  15448  o1lo1  15460  o1rlimmul  15542  lo1mul  15551  isercolllem2  15589  climcndslem1  15772  climcndslem2  15773  ruclem3  16158  ruclem9  16163  ruclem12  16166  dvdsmultr1  16223  ltoddhalfle  16288  divalglem0  16320  dvdsgcdb  16472  dfgcd2  16473  coprmgcdb  16576  coprmdvds2  16581  exprmfct  16631  prmdvdsfz  16632  prmfac1  16647  rpexp  16649  eulerthlem2  16709  pcpremul  16771  pcdvdsb  16797  pcprmpw2  16810  pockthlem  16833  prmreclem3  16846  4sqlem11  16883  vdwnnlem3  16925  meetle  18321  latjlej1  18376  latnlej2  18382  clatleglb  18441  mndodconglem  19470  efgsrel  19663  ablfac1b  20001  pgpfac1lem1  20005  lbsextlem2  21114  psdmul  22109  chfacfscmul0  22802  chfacfpmmul0  22806  lmcls  23246  ufileu  23863  ufilcmp  23976  cnpfcf  23985  tsmsxp  24099  prdsbl  24435  reconnlem2  24772  evth  24914  ivthlem2  25409  ivthlem3  25410  ovollb2lem  25445  ovoliunlem2  25460  ovolicc2lem3  25476  ismbf3d  25611  itg2seq  25699  itg2monolem1  25707  dvcnvrelem1  25978  itgsubst  26012  plypf1  26173  coeaddlem  26210  coemullem  26211  ulmcau  26360  abelth  26407  wilth  27037  ftalem2  27040  ftalem3  27041  muval1  27099  dvdssqf  27104  sqff1o  27148  chtub  27179  bposlem3  27253  lgsne0  27302  gausslemma2dlem1a  27332  gausslemma2dlem2  27334  lgseisenlem1  27342  lgseisenlem2  27343  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  lgsquad2lem1  27351  lgsquad2lem2  27352  dchrisum0lem1  27483  pntlem3  27576  negbdaylem  28052  mulsproplem5  28116  mulsproplem8  28119  bdayons  28272  z12bdaylem1  28466  upgrewlkle2  29680  pthdlem1  29839  crctcshwlkn0lem3  29885  ex-natded5.8-2  30489  nmoub3i  30848  ubthlem1  30945  ubthlem2  30946  shsel1  31396  nmopub2tALT  31984  nmfnleub2  32001  lnconi  32108  eulerpartlemb  34525  r1elcl  35254  dfon2lem4  35978  btwncomim  36207  nn0prpwlem  36516  ltflcei  37805  poimirlem9  37826  poimirlem18  37835  poimirlem21  37838  poimirlem22  37839  poimirlem24  37841  poimirlem29  37846  heicant  37852  mbfresfi  37863  itg2addnclem2  37869  itg2addnclem3  37870  incsequz  37945  heibor1lem  38006  atlelt  39694  1cvratex  39729  dalem3  39920  linepsubN  40008  pmapsub  40024  2llnma3r  40044  cdlemblem  40049  pmapjoin  40108  atmod1i1  40113  atmod1i2  40115  llnmod1i2  40116  lhpmcvr4N  40282  4atexlemnclw  40326  cdlemd3  40456  cdleme3g  40490  cdleme3h  40491  cdleme7d  40502  cdleme7ga  40504  cdleme21c  40583  cdleme35fnpq  40705  cdleme35f  40710  cdlemf1  40817  cdlemg4  40873  cdlemg6c  40876  cdlemg27a  40948  cdlemg33b0  40957  cdlemg33a  40962  cdlemk3  41089  dia2dimlem1  41320  dvheveccl  41368  dihord6apre  41512  dihord6b  41516  coprmdvdsb  43223  harval3  43775  monoordxrv  45721  stoweid  46303  smonoord  47613  iccpartgt  47669  goldbachthlem2  47788  lighneallem2  47848  tgoldbach  48059  nn0sumltlt  48592  dignn0flhalflem1  48857