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  5350  ralxfrd2  5354  sotri3  6083  predtrss  6274  oeordi  8512  coflton  8596  cofon1  8597  cofon2  8598  xpfiOLD  9228  ttrclss  9635  alephle  10001  axdc3lem4  10366  dedekindle  11298  addlsub  11554  letrp1  11986  ledivp1  12045  peano2uz2  12582  uzind  12586  xrre  13089  xrre2  13090  xrltmin  13102  xrlemin  13104  lemaxle  13115  xralrple  13125  xlemul1a  13208  xrinfmsslem  13228  flge  13727  flflp1  13729  fsequb  13900  seqcl2  13945  monoord  13957  facwordi  14214  facavg  14226  01sqrexlem6  15172  leabs  15224  caubnd  15284  limsupgre  15406  limsupbnd2  15408  lo1bdd2  15449  lo1bddrp  15450  o1lo1  15462  o1rlimmul  15544  lo1mul  15553  isercolllem2  15591  climcndslem1  15774  climcndslem2  15775  ruclem3  16160  ruclem9  16165  ruclem12  16168  dvdsmultr1  16225  ltoddhalfle  16290  divalglem0  16322  dvdsgcdb  16474  dfgcd2  16475  coprmgcdb  16578  coprmdvds2  16583  exprmfct  16633  prmdvdsfz  16634  prmfac1  16649  rpexp  16651  eulerthlem2  16711  pcpremul  16773  pcdvdsb  16799  pcprmpw2  16812  pockthlem  16835  prmreclem3  16848  4sqlem11  16885  vdwnnlem3  16927  meetle  18322  latjlej1  18377  latnlej2  18383  clatleglb  18442  mndodconglem  19438  efgsrel  19631  ablfac1b  19969  pgpfac1lem1  19973  lbsextlem2  21084  psdmul  22069  chfacfscmul0  22761  chfacfpmmul0  22765  lmcls  23205  ufileu  23822  ufilcmp  23935  cnpfcf  23944  tsmsxp  24058  prdsbl  24395  reconnlem2  24732  evth  24874  ivthlem2  25369  ivthlem3  25370  ovollb2lem  25405  ovoliunlem2  25420  ovolicc2lem3  25436  ismbf3d  25571  itg2seq  25659  itg2monolem1  25667  dvcnvrelem1  25938  itgsubst  25972  plypf1  26133  coeaddlem  26170  coemullem  26171  ulmcau  26320  abelth  26367  wilth  26997  ftalem2  27000  ftalem3  27001  muval1  27059  dvdssqf  27064  sqff1o  27108  chtub  27139  bposlem3  27213  lgsne0  27262  gausslemma2dlem1a  27292  gausslemma2dlem2  27294  lgseisenlem1  27302  lgseisenlem2  27303  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  lgsquad2lem1  27311  lgsquad2lem2  27312  dchrisum0lem1  27443  pntlem3  27536  negsbdaylem  27985  mulsproplem5  28046  mulsproplem8  28049  bdayon  28196  upgrewlkle2  29570  pthdlem1  29729  crctcshwlkn0lem3  29775  ex-natded5.8-2  30376  nmoub3i  30735  ubthlem1  30832  ubthlem2  30833  shsel1  31283  nmopub2tALT  31871  nmfnleub2  31888  lnconi  31995  eulerpartlemb  34335  dfon2lem4  35759  btwncomim  35986  nn0prpwlem  36295  ltflcei  37587  poimirlem9  37608  poimirlem18  37617  poimirlem21  37620  poimirlem22  37621  poimirlem24  37623  poimirlem29  37628  heicant  37634  mbfresfi  37645  itg2addnclem2  37651  itg2addnclem3  37652  incsequz  37727  heibor1lem  37788  atlelt  39417  1cvratex  39452  dalem3  39643  linepsubN  39731  pmapsub  39747  2llnma3r  39767  cdlemblem  39772  pmapjoin  39831  atmod1i1  39836  atmod1i2  39838  llnmod1i2  39839  lhpmcvr4N  40005  4atexlemnclw  40049  cdlemd3  40179  cdleme3g  40213  cdleme3h  40214  cdleme7d  40225  cdleme7ga  40227  cdleme21c  40306  cdleme35fnpq  40428  cdleme35f  40433  cdlemf1  40540  cdlemg4  40596  cdlemg6c  40599  cdlemg27a  40671  cdlemg33b0  40680  cdlemg33a  40685  cdlemk3  40812  dia2dimlem1  41043  dvheveccl  41091  dihord6apre  41235  dihord6b  41239  coprmdvdsb  42958  harval3  43511  monoordxrv  45461  stoweid  46045  smonoord  47356  iccpartgt  47412  goldbachthlem2  47531  lighneallem2  47591  tgoldbach  47802  nn0sumltlt  48335  dignn0flhalflem1  48601