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  5348  ralxfrd2  5352  sotri3  6081  predtrss  6274  oeordi  8508  coflton  8592  cofon1  8593  cofon2  8594  ttrclss  9617  alephle  9986  axdc3lem4  10351  dedekindle  11284  addlsub  11540  letrp1  11972  ledivp1  12031  peano2uz2  12567  uzind  12571  xrre  13070  xrre2  13071  xrltmin  13083  xrlemin  13085  lemaxle  13096  xralrple  13106  xlemul1a  13189  xrinfmsslem  13209  flge  13711  flflp1  13713  fsequb  13884  seqcl2  13929  monoord  13941  facwordi  14198  facavg  14210  01sqrexlem6  15156  leabs  15208  caubnd  15268  limsupgre  15390  limsupbnd2  15392  lo1bdd2  15433  lo1bddrp  15434  o1lo1  15446  o1rlimmul  15528  lo1mul  15537  isercolllem2  15575  climcndslem1  15758  climcndslem2  15759  ruclem3  16144  ruclem9  16149  ruclem12  16152  dvdsmultr1  16209  ltoddhalfle  16274  divalglem0  16306  dvdsgcdb  16458  dfgcd2  16459  coprmgcdb  16562  coprmdvds2  16567  exprmfct  16617  prmdvdsfz  16618  prmfac1  16633  rpexp  16635  eulerthlem2  16695  pcpremul  16757  pcdvdsb  16783  pcprmpw2  16796  pockthlem  16819  prmreclem3  16832  4sqlem11  16869  vdwnnlem3  16911  meetle  18306  latjlej1  18361  latnlej2  18367  clatleglb  18426  mndodconglem  19455  efgsrel  19648  ablfac1b  19986  pgpfac1lem1  19990  lbsextlem2  21098  psdmul  22082  chfacfscmul0  22774  chfacfpmmul0  22778  lmcls  23218  ufileu  23835  ufilcmp  23948  cnpfcf  23957  tsmsxp  24071  prdsbl  24407  reconnlem2  24744  evth  24886  ivthlem2  25381  ivthlem3  25382  ovollb2lem  25417  ovoliunlem2  25432  ovolicc2lem3  25448  ismbf3d  25583  itg2seq  25671  itg2monolem1  25679  dvcnvrelem1  25950  itgsubst  25984  plypf1  26145  coeaddlem  26182  coemullem  26183  ulmcau  26332  abelth  26379  wilth  27009  ftalem2  27012  ftalem3  27013  muval1  27071  dvdssqf  27076  sqff1o  27120  chtub  27151  bposlem3  27225  lgsne0  27274  gausslemma2dlem1a  27304  gausslemma2dlem2  27306  lgseisenlem1  27314  lgseisenlem2  27315  lgsquadlem1  27319  lgsquadlem2  27320  lgsquadlem3  27321  lgsquad2lem1  27323  lgsquad2lem2  27324  dchrisum0lem1  27455  pntlem3  27548  negsbdaylem  27999  mulsproplem5  28060  mulsproplem8  28063  bdayon  28210  upgrewlkle2  29587  pthdlem1  29746  crctcshwlkn0lem3  29792  ex-natded5.8-2  30396  nmoub3i  30755  ubthlem1  30852  ubthlem2  30853  shsel1  31303  nmopub2tALT  31891  nmfnleub2  31908  lnconi  32015  eulerpartlemb  34402  r1elcl  35130  dfon2lem4  35849  btwncomim  36078  nn0prpwlem  36387  ltflcei  37668  poimirlem9  37689  poimirlem18  37698  poimirlem21  37701  poimirlem22  37702  poimirlem24  37704  poimirlem29  37709  heicant  37715  mbfresfi  37726  itg2addnclem2  37732  itg2addnclem3  37733  incsequz  37808  heibor1lem  37869  atlelt  39557  1cvratex  39592  dalem3  39783  linepsubN  39871  pmapsub  39887  2llnma3r  39907  cdlemblem  39912  pmapjoin  39971  atmod1i1  39976  atmod1i2  39978  llnmod1i2  39979  lhpmcvr4N  40145  4atexlemnclw  40189  cdlemd3  40319  cdleme3g  40353  cdleme3h  40354  cdleme7d  40365  cdleme7ga  40367  cdleme21c  40446  cdleme35fnpq  40568  cdleme35f  40573  cdlemf1  40680  cdlemg4  40736  cdlemg6c  40739  cdlemg27a  40811  cdlemg33b0  40820  cdlemg33a  40825  cdlemk3  40952  dia2dimlem1  41183  dvheveccl  41231  dihord6apre  41375  dihord6b  41379  coprmdvdsb  43102  harval3  43655  monoordxrv  45603  stoweid  46185  smonoord  47495  iccpartgt  47551  goldbachthlem2  47670  lighneallem2  47730  tgoldbach  47941  nn0sumltlt  48474  dignn0flhalflem1  48740