Theorem mpan2d 707

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpand  708  mpan2i  710  ralxfrd  5377  ralxfrd2  5381  sotri3  6128  predtrss  6324  oeordi  8579  coflton  8663  cofon1  8664  cofon2  8665  ttrclss  9703  alephle  10095  axdc3lem4  10459  dedekindle  11402  addlsub  11658  letrp1  12087  ledivp1  12145  peano2uz2  12713  uzind  12717  xrre  13225  xrre2  13226  xrltmin  13238  xrlemin  13240  lemaxle  13251  xralrple  13261  xlemul1a  13344  xrinfmsslem  13364  flge  13870  flflp1  13872  fsequb  14043  seqcl2  14088  monoord  14100  facwordi  14357  facavg  14369  01sqrexlem6  15338  leabs  15390  caubnd  15450  limsupgre  15572  limsupbnd2  15574  lo1bdd2  15615  lo1bddrp  15616  o1lo1  15628  o1rlimmul  15710  lo1mul  15719  isercolllem2  15757  climcndslem1  15942  climcndslem2  15943  ruclem3  16327  ruclem9  16332  ruclem12  16335  dvdsmultr1  16392  ltoddhalfle  16457  divalglem0  16489  dvdsgcdb  16641  dfgcd2  16642  coprmgcdb  16745  coprmdvds2  16750  exprmfct  16801  prmdvdsfz  16802  prmfac1  16817  rpexp  16819  eulerthlem2  16879  pcpremul  16941  pcdvdsb  16967  pcprmpw2  16980  pockthlem  17003  prmreclem3  17016  4sqlem11  17053  vdwnnlem3  17095  meetle  18492  latjlej1  18547  latnlej2  18553  clatleglb  18612  mndodconglem  19674  efgsrel  19867  ablfac1b  20205  pgpfac1lem1  20209  lbsextlem2  21352  psdmul  22400  chfacfscmul0  23089  chfacfpmmul0  23093  lmcls  23533  ufileu  24151  ufilcmp  24264  cnpfcf  24273  tsmsxp  24387  prdsbl  24723  reconnlem2  25060  evth  25193  ivthlem2  25686  ivthlem3  25687  ovollb2lem  25722  ovoliunlem2  25737  ovolicc2lem3  25753  ismbf3d  25888  itg2seq  25976  itg2monolem1  25984  dvcnvrelem1  26251  itgsubst  26283  plypf1  26445  coeaddlem  26482  coemullem  26483  ulmcau  26638  abelth  26684  wilth  27315  ftalem2  27318  ftalem3  27319  muval1  27377  dvdssqf  27382  sqff1o  27426  chtub  27456  bposlem3  27530  lgsne0  27579  gausslemma2dlem1a  27609  gausslemma2dlem2  27611  lgseisenlem1  27619  lgseisenlem2  27620  lgsquadlem1  27624  lgsquadlem2  27625  lgsquadlem3  27626  lgsquad2lem1  27628  lgsquad2lem2  27629  dchrisum0lem1  27760  pntlem3  27853  negbdaylem  28329  mulsproplem5  28393  mulsproplem8  28396  bdayons  28549  z12bdaylem1  28743  upgrewlkle2  30074  pthdlem1  30239  crctcshwlkn0lem3  30288  ex-natded5.8-2  30902  nmoub3i  31262  ubthlem1  31359  ubthlem2  31360  shsel1  31810  nmopub2tALT  32398  nmfnleub2  32415  lnconi  32522  eulerpartlemb  34887  r1elcl  35613  karddom  35695  kardsdom  35696  dfon2lem4  36371  btwncomim  36601  ltnmul  36804  nn0prpwlem  36949  cgsex2gd  37897  ltflcei  38370  poimirlem9  38386  poimirlem18  38395  poimirlem21  38398  poimirlem22  38399  poimirlem24  38401  poimirlem29  38406  heicant  38412  mbfresfi  38423  itg2addnclem2  38429  itg2addnclem3  38430  incsequz  38506  heibor1lem  38567  atlelt  40319  1cvratex  40354  dalem3  40545  linepsubN  40633  pmapsub  40649  2llnma3r  40669  cdlemblem  40674  pmapjoin  40733  atmod1i1  40738  atmod1i2  40740  llnmod1i2  40741  lhpmcvr4N  40907  4atexlemnclw  40951  cdlemd3  41081  cdleme3g  41115  cdleme3h  41116  cdleme7d  41127  cdleme7ga  41129  cdleme21c  41208  cdleme35fnpq  41330  cdleme35f  41335  cdlemf1  41442  cdlemg4  41498  cdlemg6c  41501  cdlemg27a  41573  cdlemg33b0  41582  cdlemg33a  41587  cdlemk3  41714  dia2dimlem1  41945  dvheveccl  41993  dihord6apre  42137  dihord6b  42141  coprmdvdsb  43834  harval3  44386  monoordxrv  46317  stoweid  46899  smonoord  48273  iccpartgt  48335  goldbachthlem2  48457  lighneallem2  48517  tgoldbach  48741  nn0sumltlt  49288  dignn0flhalflem1  49553