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  5366  ralxfrd2  5370  sotri3  6106  predtrss  6298  oeordi  8554  coflton  8638  cofon1  8639  cofon2  8640  xpfiOLD  9277  ttrclss  9680  alephle  10048  axdc3lem4  10413  dedekindle  11345  addlsub  11601  letrp1  12033  ledivp1  12092  peano2uz2  12629  uzind  12633  xrre  13136  xrre2  13137  xrltmin  13149  xrlemin  13151  lemaxle  13162  xralrple  13172  xlemul1a  13255  xrinfmsslem  13275  flge  13774  flflp1  13776  fsequb  13947  seqcl2  13992  monoord  14004  facwordi  14261  facavg  14273  01sqrexlem6  15220  leabs  15272  caubnd  15332  limsupgre  15454  limsupbnd2  15456  lo1bdd2  15497  lo1bddrp  15498  o1lo1  15510  o1rlimmul  15592  lo1mul  15601  isercolllem2  15639  climcndslem1  15822  climcndslem2  15823  ruclem3  16208  ruclem9  16213  ruclem12  16216  dvdsmultr1  16273  ltoddhalfle  16338  divalglem0  16370  dvdsgcdb  16522  dfgcd2  16523  coprmgcdb  16626  coprmdvds2  16631  exprmfct  16681  prmdvdsfz  16682  prmfac1  16697  rpexp  16699  eulerthlem2  16759  pcpremul  16821  pcdvdsb  16847  pcprmpw2  16860  pockthlem  16883  prmreclem3  16896  4sqlem11  16933  vdwnnlem3  16975  meetle  18366  latjlej1  18419  latnlej2  18425  clatleglb  18484  mndodconglem  19478  efgsrel  19671  ablfac1b  20009  pgpfac1lem1  20013  lbsextlem2  21076  psdmul  22060  chfacfscmul0  22752  chfacfpmmul0  22756  lmcls  23196  ufileu  23813  ufilcmp  23926  cnpfcf  23935  tsmsxp  24049  prdsbl  24386  reconnlem2  24723  evth  24865  ivthlem2  25360  ivthlem3  25361  ovollb2lem  25396  ovoliunlem2  25411  ovolicc2lem3  25427  ismbf3d  25562  itg2seq  25650  itg2monolem1  25658  dvcnvrelem1  25929  itgsubst  25963  plypf1  26124  coeaddlem  26161  coemullem  26162  ulmcau  26311  abelth  26358  wilth  26988  ftalem2  26991  ftalem3  26992  muval1  27050  dvdssqf  27055  sqff1o  27099  chtub  27130  bposlem3  27204  lgsne0  27253  gausslemma2dlem1a  27283  gausslemma2dlem2  27285  lgseisenlem1  27293  lgseisenlem2  27294  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  lgsquad2lem1  27302  lgsquad2lem2  27303  dchrisum0lem1  27434  pntlem3  27527  negsbdaylem  27969  mulsproplem5  28030  mulsproplem8  28033  bdayon  28180  upgrewlkle2  29541  pthdlem1  29703  crctcshwlkn0lem3  29749  ex-natded5.8-2  30350  nmoub3i  30709  ubthlem1  30806  ubthlem2  30807  shsel1  31257  nmopub2tALT  31845  nmfnleub2  31862  lnconi  31969  eulerpartlemb  34366  dfon2lem4  35781  btwncomim  36008  nn0prpwlem  36317  ltflcei  37609  poimirlem9  37630  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  poimirlem24  37645  poimirlem29  37650  heicant  37656  mbfresfi  37667  itg2addnclem2  37673  itg2addnclem3  37674  incsequz  37749  heibor1lem  37810  atlelt  39439  1cvratex  39474  dalem3  39665  linepsubN  39753  pmapsub  39769  2llnma3r  39789  cdlemblem  39794  pmapjoin  39853  atmod1i1  39858  atmod1i2  39860  llnmod1i2  39861  lhpmcvr4N  40027  4atexlemnclw  40071  cdlemd3  40201  cdleme3g  40235  cdleme3h  40236  cdleme7d  40247  cdleme7ga  40249  cdleme21c  40328  cdleme35fnpq  40450  cdleme35f  40455  cdlemf1  40562  cdlemg4  40618  cdlemg6c  40621  cdlemg27a  40693  cdlemg33b0  40702  cdlemg33a  40707  cdlemk3  40834  dia2dimlem1  41065  dvheveccl  41113  dihord6apre  41257  dihord6b  41261  coprmdvdsb  42981  harval3  43534  monoordxrv  45484  stoweid  46068  smonoord  47376  iccpartgt  47432  goldbachthlem2  47551  lighneallem2  47611  tgoldbach  47822  nn0sumltlt  48342  dignn0flhalflem1  48608