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  5355  ralxfrd2  5359  sotri3  6095  predtrss  6288  oeordi  8525  coflton  8609  cofon1  8610  cofon2  8611  ttrclss  9641  alephle  10010  axdc3lem4  10375  dedekindle  11309  addlsub  11565  letrp1  11997  ledivp1  12056  peano2uz2  12592  uzind  12596  xrre  13096  xrre2  13097  xrltmin  13109  xrlemin  13111  lemaxle  13122  xralrple  13132  xlemul1a  13215  xrinfmsslem  13235  flge  13737  flflp1  13739  fsequb  13910  seqcl2  13955  monoord  13967  facwordi  14224  facavg  14236  01sqrexlem6  15182  leabs  15234  caubnd  15294  limsupgre  15416  limsupbnd2  15418  lo1bdd2  15459  lo1bddrp  15460  o1lo1  15472  o1rlimmul  15554  lo1mul  15563  isercolllem2  15601  climcndslem1  15784  climcndslem2  15785  ruclem3  16170  ruclem9  16175  ruclem12  16178  dvdsmultr1  16235  ltoddhalfle  16300  divalglem0  16332  dvdsgcdb  16484  dfgcd2  16485  coprmgcdb  16588  coprmdvds2  16593  exprmfct  16643  prmdvdsfz  16644  prmfac1  16659  rpexp  16661  eulerthlem2  16721  pcpremul  16783  pcdvdsb  16809  pcprmpw2  16822  pockthlem  16845  prmreclem3  16858  4sqlem11  16895  vdwnnlem3  16937  meetle  18333  latjlej1  18388  latnlej2  18394  clatleglb  18453  mndodconglem  19482  efgsrel  19675  ablfac1b  20013  pgpfac1lem1  20017  lbsextlem2  21126  psdmul  22121  chfacfscmul0  22814  chfacfpmmul0  22818  lmcls  23258  ufileu  23875  ufilcmp  23988  cnpfcf  23997  tsmsxp  24111  prdsbl  24447  reconnlem2  24784  evth  24926  ivthlem2  25421  ivthlem3  25422  ovollb2lem  25457  ovoliunlem2  25472  ovolicc2lem3  25488  ismbf3d  25623  itg2seq  25711  itg2monolem1  25719  dvcnvrelem1  25990  itgsubst  26024  plypf1  26185  coeaddlem  26222  coemullem  26223  ulmcau  26372  abelth  26419  wilth  27049  ftalem2  27052  ftalem3  27053  muval1  27111  dvdssqf  27116  sqff1o  27160  chtub  27191  bposlem3  27265  lgsne0  27314  gausslemma2dlem1a  27344  gausslemma2dlem2  27346  lgseisenlem1  27354  lgseisenlem2  27355  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  lgsquad2lem1  27363  lgsquad2lem2  27364  dchrisum0lem1  27495  pntlem3  27588  negbdaylem  28064  mulsproplem5  28128  mulsproplem8  28131  bdayons  28284  z12bdaylem1  28478  upgrewlkle2  29692  pthdlem1  29851  crctcshwlkn0lem3  29897  ex-natded5.8-2  30501  nmoub3i  30860  ubthlem1  30957  ubthlem2  30958  shsel1  31408  nmopub2tALT  31996  nmfnleub2  32013  lnconi  32120  eulerpartlemb  34545  r1elcl  35273  dfon2lem4  35997  btwncomim  36226  nn0prpwlem  36535  cgsex2gd  37386  ltflcei  37853  poimirlem9  37874  poimirlem18  37883  poimirlem21  37886  poimirlem22  37887  poimirlem24  37889  poimirlem29  37894  heicant  37900  mbfresfi  37911  itg2addnclem2  37917  itg2addnclem3  37918  incsequz  37993  heibor1lem  38054  atlelt  39808  1cvratex  39843  dalem3  40034  linepsubN  40122  pmapsub  40138  2llnma3r  40158  cdlemblem  40163  pmapjoin  40222  atmod1i1  40227  atmod1i2  40229  llnmod1i2  40230  lhpmcvr4N  40396  4atexlemnclw  40440  cdlemd3  40570  cdleme3g  40604  cdleme3h  40605  cdleme7d  40616  cdleme7ga  40618  cdleme21c  40697  cdleme35fnpq  40819  cdleme35f  40824  cdlemf1  40931  cdlemg4  40987  cdlemg6c  40990  cdlemg27a  41062  cdlemg33b0  41071  cdlemg33a  41076  cdlemk3  41203  dia2dimlem1  41434  dvheveccl  41482  dihord6apre  41626  dihord6b  41630  coprmdvdsb  43336  harval3  43888  monoordxrv  45833  stoweid  46415  smonoord  47725  iccpartgt  47781  goldbachthlem2  47900  lighneallem2  47960  tgoldbach  48171  nn0sumltlt  48704  dignn0flhalflem1  48969