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  5384  ralxfrd2  5388  sotri3  6135  predtrss  6330  oeordi  8582  coflton  8666  cofon1  8667  cofon2  8668  ttrclss  9699  alephle  10091  axdc3lem4  10455  dedekindle  11392  addlsub  11648  letrp1  12077  ledivp1  12135  peano2uz2  12702  uzind  12706  xrre  13213  xrre2  13214  xrltmin  13226  xrlemin  13228  lemaxle  13239  xralrple  13249  xlemul1a  13332  xrinfmsslem  13352  flge  13858  flflp1  13860  fsequb  14031  seqcl2  14076  monoord  14088  facwordi  14345  facavg  14357  01sqrexlem6  15324  leabs  15376  caubnd  15436  limsupgre  15558  limsupbnd2  15560  lo1bdd2  15601  lo1bddrp  15602  o1lo1  15614  o1rlimmul  15696  lo1mul  15705  isercolllem2  15743  climcndslem1  15929  climcndslem2  15930  ruclem3  16314  ruclem9  16319  ruclem12  16322  dvdsmultr1  16379  ltoddhalfle  16444  divalglem0  16476  dvdsgcdb  16628  dfgcd2  16629  coprmgcdb  16732  coprmdvds2  16737  exprmfct  16788  prmdvdsfz  16789  prmfac1  16804  rpexp  16806  eulerthlem2  16866  pcpremul  16928  pcdvdsb  16954  pcprmpw2  16967  pockthlem  16990  prmreclem3  17003  4sqlem11  17040  vdwnnlem3  17082  meetle  18479  latjlej1  18534  latnlej2  18540  clatleglb  18599  mndodconglem  19642  efgsrel  19835  ablfac1b  20173  pgpfac1lem1  20177  lbsextlem2  21320  psdmul  22366  chfacfscmul0  23052  chfacfpmmul0  23056  lmcls  23496  ufileu  24113  ufilcmp  24226  cnpfcf  24235  tsmsxp  24349  prdsbl  24685  reconnlem2  25022  evth  25155  ivthlem2  25648  ivthlem3  25649  ovollb2lem  25684  ovoliunlem2  25699  ovolicc2lem3  25715  ismbf3d  25850  itg2seq  25938  itg2monolem1  25946  dvcnvrelem1  26213  itgsubst  26245  plypf1  26406  coeaddlem  26443  coemullem  26444  ulmcau  26595  abelth  26641  wilth  27272  ftalem2  27275  ftalem3  27276  muval1  27334  dvdssqf  27339  sqff1o  27383  chtub  27413  bposlem3  27487  lgsne0  27536  gausslemma2dlem1a  27566  gausslemma2dlem2  27568  lgseisenlem1  27576  lgseisenlem2  27577  lgsquadlem1  27581  lgsquadlem2  27582  lgsquadlem3  27583  lgsquad2lem1  27585  lgsquad2lem2  27586  dchrisum0lem1  27717  pntlem3  27810  negbdaylem  28286  mulsproplem5  28350  mulsproplem8  28353  bdayons  28506  z12bdaylem1  28700  upgrewlkle2  29993  pthdlem1  30152  crctcshwlkn0lem3  30198  ex-natded5.8-2  30802  nmoub3i  31162  ubthlem1  31259  ubthlem2  31260  shsel1  31710  nmopub2tALT  32298  nmfnleub2  32315  lnconi  32422  eulerpartlemb  34790  r1elcl  35516  karddom  35598  kardsdom  35599  dfon2lem4  36297  btwncomim  36526  ltnmul  36729  nn0prpwlem  36874  cgsex2gd  37822  ltflcei  38300  poimirlem9  38321  poimirlem18  38330  poimirlem21  38333  poimirlem22  38334  poimirlem24  38336  poimirlem29  38341  heicant  38347  mbfresfi  38358  itg2addnclem2  38364  itg2addnclem3  38365  incsequz  38440  heibor1lem  38501  atlelt  40253  1cvratex  40288  dalem3  40479  linepsubN  40567  pmapsub  40583  2llnma3r  40603  cdlemblem  40608  pmapjoin  40667  atmod1i1  40672  atmod1i2  40674  llnmod1i2  40675  lhpmcvr4N  40841  4atexlemnclw  40885  cdlemd3  41015  cdleme3g  41049  cdleme3h  41050  cdleme7d  41061  cdleme7ga  41063  cdleme21c  41142  cdleme35fnpq  41264  cdleme35f  41269  cdlemf1  41376  cdlemg4  41432  cdlemg6c  41435  cdlemg27a  41507  cdlemg33b0  41516  cdlemg33a  41521  cdlemk3  41648  dia2dimlem1  41879  dvheveccl  41927  dihord6apre  42071  dihord6b  42075  coprmdvdsb  43753  harval3  44305  monoordxrv  46236  stoweid  46818  smonoord  48155  iccpartgt  48217  goldbachthlem2  48339  lighneallem2  48399  tgoldbach  48623  nn0sumltlt  49171  dignn0flhalflem1  49436