Theorem mpan2d 701

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 417	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpid 44	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397

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 209  df-an 398

This theorem is referenced by:  mpand  702  mpan2i  704  ralxfrd  5340  ralxfrd2  5344  sotri3  6087  predtrss  6277  oeordi  8517  coflton  8601  cofon1  8602  cofon2  8603  ttrclss  9636  alephle  10005  axdc3lem4  10370  dedekindle  11305  addlsub  11561  letrp1  11994  ledivp1  12053  peano2uz2  12612  uzind  12616  xrre  13116  xrre2  13117  xrltmin  13129  xrlemin  13131  lemaxle  13142  xralrple  13152  xlemul1a  13235  xrinfmsslem  13255  flge  13759  flflp1  13761  fsequb  13932  seqcl2  13977  monoord  13989  facwordi  14246  facavg  14258  01sqrexlem6  15204  leabs  15256  caubnd  15316  limsupgre  15438  limsupbnd2  15440  lo1bdd2  15481  lo1bddrp  15482  o1lo1  15494  o1rlimmul  15576  lo1mul  15585  isercolllem2  15623  climcndslem1  15809  climcndslem2  15810  ruclem3  16195  ruclem9  16200  ruclem12  16203  dvdsmultr1  16260  ltoddhalfle  16325  divalglem0  16357  dvdsgcdb  16509  dfgcd2  16510  coprmgcdb  16613  coprmdvds2  16618  exprmfct  16669  prmdvdsfz  16670  prmfac1  16685  rpexp  16687  eulerthlem2  16747  pcpremul  16809  pcdvdsb  16835  pcprmpw2  16848  pockthlem  16871  prmreclem3  16884  4sqlem11  16921  vdwnnlem3  16963  meetle  18359  latjlej1  18414  latnlej2  18420  clatleglb  18479  mndodconglem  19511  efgsrel  19704  ablfac1b  20042  pgpfac1lem1  20046  lbsextlem2  21156  psdmul  22158  chfacfscmul0  22845  chfacfpmmul0  22849  lmcls  23289  ufileu  23906  ufilcmp  24019  cnpfcf  24028  tsmsxp  24142  prdsbl  24478  reconnlem2  24815  evth  24948  ivthlem2  25441  ivthlem3  25442  ovollb2lem  25477  ovoliunlem2  25492  ovolicc2lem3  25508  ismbf3d  25643  itg2seq  25731  itg2monolem1  25739  dvcnvrelem1  26006  itgsubst  26038  plypf1  26199  coeaddlem  26236  coemullem  26237  ulmcau  26382  abelth  26428  wilth  27056  ftalem2  27059  ftalem3  27060  muval1  27118  dvdssqf  27123  sqff1o  27167  chtub  27197  bposlem3  27271  lgsne0  27320  gausslemma2dlem1a  27350  gausslemma2dlem2  27352  lgseisenlem1  27360  lgseisenlem2  27361  lgsquadlem1  27365  lgsquadlem2  27366  lgsquadlem3  27367  lgsquad2lem1  27369  lgsquad2lem2  27370  dchrisum0lem1  27501  pntlem3  27594  negbdaylem  28070  mulsproplem5  28134  mulsproplem8  28137  bdayons  28290  z12bdaylem1  28484  upgrewlkle2  29697  pthdlem1  29856  crctcshwlkn0lem3  29902  ex-natded5.8-2  30506  nmoub3i  30866  ubthlem1  30963  ubthlem2  30964  shsel1  31414  nmopub2tALT  32002  nmfnleub2  32019  lnconi  32126  eulerpartlemb  34564  r1elcl  35294  dfon2lem4  36027  btwncomim  36256  nn0prpwlem  36565  cgsex2gd  37512  ltflcei  37990  poimirlem9  38011  poimirlem18  38020  poimirlem21  38023  poimirlem22  38024  poimirlem24  38026  poimirlem29  38031  heicant  38037  mbfresfi  38048  itg2addnclem2  38054  itg2addnclem3  38055  incsequz  38130  heibor1lem  38191  atlelt  39945  1cvratex  39980  dalem3  40171  linepsubN  40259  pmapsub  40275  2llnma3r  40295  cdlemblem  40300  pmapjoin  40359  atmod1i1  40364  atmod1i2  40366  llnmod1i2  40367  lhpmcvr4N  40533  4atexlemnclw  40577  cdlemd3  40707  cdleme3g  40741  cdleme3h  40742  cdleme7d  40753  cdleme7ga  40755  cdleme21c  40834  cdleme35fnpq  40956  cdleme35f  40961  cdlemf1  41068  cdlemg4  41124  cdlemg6c  41127  cdlemg27a  41199  cdlemg33b0  41208  cdlemg33a  41213  cdlemk3  41340  dia2dimlem1  41571  dvheveccl  41619  dihord6apre  41763  dihord6b  41767  coprmdvdsb  43445  harval3  43997  monoordxrv  45938  stoweid  46520  smonoord  47854  iccpartgt  47916  goldbachthlem2  48038  lighneallem2  48098  tgoldbach  48322  nn0sumltlt  48855  dignn0flhalflem1  49120