Theorem mpan2d 693

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mpand  694  mpan2i  696  ralxfrd  5407  ralxfrd2  5411  sotri3  6132  predtrss  6324  oeordi  8587  coflton  8670  cofon1  8671  cofon2  8672  xpfiOLD  9318  ttrclss  9715  alephle  10083  axdc3lem4  10448  dedekindle  11378  addlsub  11630  letrp1  12058  ledivp1  12116  peano2uz2  12650  uzind  12654  xrre  13148  xrre2  13149  xrltmin  13161  xrlemin  13163  lemaxle  13174  xralrple  13184  xlemul1a  13267  xrinfmsslem  13287  flge  13770  flflp1  13772  fsequb  13940  seqcl2  13986  monoord  13998  facwordi  14249  facavg  14261  01sqrexlem6  15194  leabs  15246  caubnd  15305  limsupgre  15425  limsupbnd2  15427  lo1bdd2  15468  lo1bddrp  15469  o1lo1  15481  o1rlimmul  15563  lo1mul  15572  isercolllem2  15612  climcndslem1  15795  climcndslem2  15796  ruclem3  16176  ruclem9  16181  ruclem12  16184  dvdsmultr1  16239  ltoddhalfle  16304  divalglem0  16336  dvdsgcdb  16487  dfgcd2  16488  coprmgcdb  16586  coprmdvds2  16591  exprmfct  16641  prmdvdsfz  16642  prmfac1  16658  rpexp  16659  eulerthlem2  16715  pcpremul  16776  pcdvdsb  16802  pcprmpw2  16815  pockthlem  16838  prmreclem3  16851  4sqlem11  16888  vdwnnlem3  16930  meetle  18353  latjlej1  18406  latnlej2  18412  clatleglb  18471  mndodconglem  19409  efgsrel  19602  ablfac1b  19940  pgpfac1lem1  19944  lbsextlem2  20772  chfacfscmul0  22360  chfacfpmmul0  22364  lmcls  22806  ufileu  23423  ufilcmp  23536  cnpfcf  23545  tsmsxp  23659  prdsbl  24000  reconnlem2  24343  evth  24475  ivthlem2  24969  ivthlem3  24970  ovollb2lem  25005  ovoliunlem2  25020  ovolicc2lem3  25036  ismbf3d  25171  itg2seq  25260  itg2monolem1  25268  dvcnvrelem1  25534  itgsubst  25566  plypf1  25726  coeaddlem  25763  coemullem  25764  ulmcau  25907  abelth  25953  wilth  26575  ftalem2  26578  ftalem3  26579  muval1  26637  dvdssqf  26642  sqff1o  26686  chtub  26715  bposlem3  26789  lgsne0  26838  gausslemma2dlem1a  26868  gausslemma2dlem2  26870  lgseisenlem1  26878  lgseisenlem2  26879  lgsquadlem1  26883  lgsquadlem2  26884  lgsquadlem3  26885  lgsquad2lem1  26887  lgsquad2lem2  26888  dchrisum0lem1  27019  pntlem3  27112  negsbdaylem  27533  mulsproplem5  27579  mulsproplem8  27582  upgrewlkle2  28894  pthdlem1  29054  crctcshwlkn0lem3  29097  ex-natded5.8-2  29698  nmoub3i  30057  ubthlem1  30154  ubthlem2  30155  shsel1  30605  nmopub2tALT  31193  nmfnleub2  31210  lnconi  31317  eulerpartlemb  33398  dfon2lem4  34789  btwncomim  35016  nn0prpwlem  35255  ltflcei  36524  poimirlem9  36545  poimirlem18  36554  poimirlem21  36557  poimirlem22  36558  poimirlem24  36560  poimirlem29  36565  heicant  36571  mbfresfi  36582  itg2addnclem2  36588  itg2addnclem3  36589  incsequz  36664  heibor1lem  36725  atlelt  38357  1cvratex  38392  dalem3  38583  linepsubN  38671  pmapsub  38687  2llnma3r  38707  cdlemblem  38712  pmapjoin  38771  atmod1i1  38776  atmod1i2  38778  llnmod1i2  38779  lhpmcvr4N  38945  4atexlemnclw  38989  cdlemd3  39119  cdleme3g  39153  cdleme3h  39154  cdleme7d  39165  cdleme7ga  39167  cdleme21c  39246  cdleme35fnpq  39368  cdleme35f  39373  cdlemf1  39480  cdlemg4  39536  cdlemg6c  39539  cdlemg27a  39611  cdlemg33b0  39620  cdlemg33a  39625  cdlemk3  39752  dia2dimlem1  39983  dvheveccl  40031  dihord6apre  40175  dihord6b  40179  coprmdvdsb  41772  harval3  42337  monoordxrv  44240  stoweid  44827  smonoord  46087  iccpartgt  46143  goldbachthlem2  46262  lighneallem2  46322  tgoldbach  46533  nn0sumltlt  47074  dignn0flhalflem1  47349