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  5369  ralxfrd2  5373  sotri3  6123  predtrss  6325  oeordi  8599  coflton  8683  cofon1  8684  cofon2  8685  ttrclss  9724  alephle  10170  axdc3lem4  10534  dedekindle  11477  addlsub  11735  letrp1  12164  ledivp1  12222  peano2uz2  12790  uzind  12794  xrre  13302  xrre2  13303  xrltmin  13315  xrlemin  13317  lemaxle  13328  xralrple  13338  xlemul1a  13421  xrinfmsslem  13441  flge  13948  flflp1  13950  fsequb  14121  seqcl2  14166  monoord  14178  facwordi  14436  facavg  14448  01sqrexlem6  15419  leabs  15471  caubnd  15531  limsupgre  15653  limsupbnd2  15655  lo1bdd2  15696  lo1bddrp  15697  o1lo1  15709  o1rlimmul  15791  lo1mul  15800  isercolllem2  15838  climcndslem1  16023  climcndslem2  16024  ruclem3  16406  ruclem9  16411  ruclem12  16414  dvdsmultr1  16471  ltoddhalfle  16536  divalglem0  16568  dvdsgcdb  16723  dfgcd2  16724  coprmgcdb  16829  coprmdvds2  16834  exprmfct  16885  prmdvdsfz  16886  prmfac1  16901  rpexp  16903  eulerthlem2  16964  pcpremul  17026  pcdvdsb  17052  pcprmpw2  17065  pockthlem  17088  prmreclem3  17101  4sqlem11  17138  vdwnnlem3  17180  meetle  18577  latjlej1  18632  latnlej2  18638  clatleglb  18697  mndodconglem  19760  efgsrel  19953  ablfac1b  20291  pgpfac1lem1  20295  lbsextlem2  21442  psdmul  22492  chfacfscmul0  23181  chfacfpmmul0  23185  lmcls  23625  ufileu  24243  ufilcmp  24356  cnpfcf  24365  tsmsxp  24479  prdsbl  24815  reconnlem2  25152  evth  25285  ivthlem2  25778  ivthlem3  25779  ovollb2lem  25814  ovoliunlem2  25829  ovolicc2lem3  25845  ismbf3d  25980  itg2seq  26068  itg2monolem1  26076  dvcnvrelem1  26342  itgsubst  26374  plypf1  26536  coeaddlem  26573  coemullem  26574  ulmcau  26727  abelth  26773  wilth  27403  ftalem2  27406  ftalem3  27407  muval1  27465  dvdssqf  27470  sqff1o  27514  chtub  27544  bposlem3  27618  lgsne0  27667  gausslemma2dlem1a  27697  gausslemma2dlem2  27699  lgseisenlem1  27707  lgseisenlem2  27708  lgsquadlem1  27712  lgsquadlem2  27713  lgsquadlem3  27714  lgsquad2lem1  27716  lgsquad2lem2  27717  dchrisum0lem1  27848  pntlem3  27941  negbdaylem  28447  mulsproplem5  28511  mulsproplem8  28514  bdayons  28667  z12bdaylem1  28861  upgrewlkle2  30192  pthdlem1  30357  crctcshwlkn0lem3  30406  ex-natded5.8-2  31020  nmoub3i  31380  ubthlem1  31477  ubthlem2  31478  shsel1  31928  nmopub2tALT  32516  nmfnleub2  32533  lnconi  32640  eulerpartlemb  35046  karddom  35885  kardsdom  35886  dfon2lem4  36640  btwncomim  36870  ltnmul  37057  nn0prpwlem  37202  cgsex2gd  38151  ltflcei  38624  poimirlem9  38640  poimirlem18  38649  poimirlem21  38652  poimirlem22  38653  poimirlem24  38655  poimirlem29  38660  heicant  38666  mbfresfi  38677  itg2addnclem2  38683  itg2addnclem3  38684  incsequz  38775  heibor1lem  38836  atlelt  40588  1cvratex  40623  dalem3  40814  linepsubN  40902  pmapsub  40918  2llnma3r  40938  cdlemblem  40943  pmapjoin  41002  atmod1i1  41007  atmod1i2  41009  llnmod1i2  41010  lhpmcvr4N  41176  4atexlemnclw  41220  cdlemd3  41350  cdleme3g  41384  cdleme3h  41385  cdleme7d  41396  cdleme7ga  41398  cdleme21c  41477  cdleme35fnpq  41599  cdleme35f  41604  cdlemf1  41711  cdlemg4  41767  cdlemg6c  41770  cdlemg27a  41842  cdlemg33b0  41851  cdlemg33a  41856  cdlemk3  41983  dia2dimlem1  42214  dvheveccl  42262  dihord6apre  42406  dihord6b  42410  coprmdvdsb  44085  harval3  44632  monoordxrv  46584  stoweid  47166  smonoord  48540  iccpartgt  48602  goldbachthlem2  48724  lighneallem2  48784  tgoldbach  49008  nn0sumltlt  49555  dignn0flhalflem1  49820