Theorem mpan2d 695

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  696  mpan2i  698  ralxfrd  5345  ralxfrd2  5349  sotri3  6087  predtrss  6280  oeordi  8516  coflton  8600  cofon1  8601  cofon2  8602  ttrclss  9632  alephle  10001  axdc3lem4  10366  dedekindle  11301  addlsub  11557  letrp1  11990  ledivp1  12049  peano2uz2  12608  uzind  12612  xrre  13112  xrre2  13113  xrltmin  13125  xrlemin  13127  lemaxle  13138  xralrple  13148  xlemul1a  13231  xrinfmsslem  13251  flge  13755  flflp1  13757  fsequb  13928  seqcl2  13973  monoord  13985  facwordi  14242  facavg  14254  01sqrexlem6  15200  leabs  15252  caubnd  15312  limsupgre  15434  limsupbnd2  15436  lo1bdd2  15477  lo1bddrp  15478  o1lo1  15490  o1rlimmul  15572  lo1mul  15581  isercolllem2  15619  climcndslem1  15805  climcndslem2  15806  ruclem3  16191  ruclem9  16196  ruclem12  16199  dvdsmultr1  16256  ltoddhalfle  16321  divalglem0  16353  dvdsgcdb  16505  dfgcd2  16506  coprmgcdb  16609  coprmdvds2  16614  exprmfct  16665  prmdvdsfz  16666  prmfac1  16681  rpexp  16683  eulerthlem2  16743  pcpremul  16805  pcdvdsb  16831  pcprmpw2  16844  pockthlem  16867  prmreclem3  16880  4sqlem11  16917  vdwnnlem3  16959  meetle  18355  latjlej1  18410  latnlej2  18416  clatleglb  18475  mndodconglem  19507  efgsrel  19700  ablfac1b  20038  pgpfac1lem1  20042  lbsextlem2  21149  psdmul  22142  chfacfscmul0  22833  chfacfpmmul0  22837  lmcls  23277  ufileu  23894  ufilcmp  24007  cnpfcf  24016  tsmsxp  24130  prdsbl  24466  reconnlem2  24803  evth  24936  ivthlem2  25429  ivthlem3  25430  ovollb2lem  25465  ovoliunlem2  25480  ovolicc2lem3  25496  ismbf3d  25631  itg2seq  25719  itg2monolem1  25727  dvcnvrelem1  25994  itgsubst  26026  plypf1  26187  coeaddlem  26224  coemullem  26225  ulmcau  26373  abelth  26419  wilth  27048  ftalem2  27051  ftalem3  27052  muval1  27110  dvdssqf  27115  sqff1o  27159  chtub  27189  bposlem3  27263  lgsne0  27312  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  lgseisenlem1  27352  lgseisenlem2  27353  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  lgsquad2lem1  27361  lgsquad2lem2  27362  dchrisum0lem1  27493  pntlem3  27586  negbdaylem  28062  mulsproplem5  28126  mulsproplem8  28129  bdayons  28282  z12bdaylem1  28476  upgrewlkle2  29690  pthdlem1  29849  crctcshwlkn0lem3  29895  ex-natded5.8-2  30499  nmoub3i  30859  ubthlem1  30956  ubthlem2  30957  shsel1  31407  nmopub2tALT  31995  nmfnleub2  32012  lnconi  32119  eulerpartlemb  34528  r1elcl  35257  dfon2lem4  35982  btwncomim  36211  nn0prpwlem  36520  cgsex2gd  37467  ltflcei  37943  poimirlem9  37964  poimirlem18  37973  poimirlem21  37976  poimirlem22  37977  poimirlem24  37979  poimirlem29  37984  heicant  37990  mbfresfi  38001  itg2addnclem2  38007  itg2addnclem3  38008  incsequz  38083  heibor1lem  38144  atlelt  39898  1cvratex  39933  dalem3  40124  linepsubN  40212  pmapsub  40228  2llnma3r  40248  cdlemblem  40253  pmapjoin  40312  atmod1i1  40317  atmod1i2  40319  llnmod1i2  40320  lhpmcvr4N  40486  4atexlemnclw  40530  cdlemd3  40660  cdleme3g  40694  cdleme3h  40695  cdleme7d  40706  cdleme7ga  40708  cdleme21c  40787  cdleme35fnpq  40909  cdleme35f  40914  cdlemf1  41021  cdlemg4  41077  cdlemg6c  41080  cdlemg27a  41152  cdlemg33b0  41161  cdlemg33a  41166  cdlemk3  41293  dia2dimlem1  41524  dvheveccl  41572  dihord6apre  41716  dihord6b  41720  coprmdvdsb  43431  harval3  43983  monoordxrv  45927  stoweid  46509  smonoord  47837  iccpartgt  47899  goldbachthlem2  48021  lighneallem2  48081  tgoldbach  48305  nn0sumltlt  48838  dignn0flhalflem1  49103