Theorem mpan2d 700

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpand  701  mpan2i  703  ralxfrd  5344  ralxfrd2  5348  sotri3  6087  predtrss  6280  oeordi  8520  coflton  8604  cofon1  8605  cofon2  8606  ttrclss  9639  alephle  10008  axdc3lem4  10373  dedekindle  11308  addlsub  11564  letrp1  11997  ledivp1  12056  peano2uz2  12615  uzind  12619  xrre  13119  xrre2  13120  xrltmin  13132  xrlemin  13134  lemaxle  13145  xralrple  13155  xlemul1a  13238  xrinfmsslem  13258  flge  13762  flflp1  13764  fsequb  13935  seqcl2  13980  monoord  13992  facwordi  14249  facavg  14261  01sqrexlem6  15207  leabs  15259  caubnd  15319  limsupgre  15441  limsupbnd2  15443  lo1bdd2  15484  lo1bddrp  15485  o1lo1  15497  o1rlimmul  15579  lo1mul  15588  isercolllem2  15626  climcndslem1  15812  climcndslem2  15813  ruclem3  16198  ruclem9  16203  ruclem12  16206  dvdsmultr1  16263  ltoddhalfle  16328  divalglem0  16360  dvdsgcdb  16512  dfgcd2  16513  coprmgcdb  16616  coprmdvds2  16621  exprmfct  16672  prmdvdsfz  16673  prmfac1  16688  rpexp  16690  eulerthlem2  16750  pcpremul  16812  pcdvdsb  16838  pcprmpw2  16851  pockthlem  16874  prmreclem3  16887  4sqlem11  16924  vdwnnlem3  16966  meetle  18362  latjlej1  18417  latnlej2  18423  clatleglb  18482  mndodconglem  19514  efgsrel  19707  ablfac1b  20045  pgpfac1lem1  20049  lbsextlem2  21159  psdmul  22161  chfacfscmul0  22848  chfacfpmmul0  22852  lmcls  23292  ufileu  23909  ufilcmp  24022  cnpfcf  24031  tsmsxp  24145  prdsbl  24481  reconnlem2  24818  evth  24951  ivthlem2  25444  ivthlem3  25445  ovollb2lem  25480  ovoliunlem2  25495  ovolicc2lem3  25511  ismbf3d  25646  itg2seq  25734  itg2monolem1  25742  dvcnvrelem1  26009  itgsubst  26041  plypf1  26202  coeaddlem  26239  coemullem  26240  ulmcau  26385  abelth  26431  wilth  27059  ftalem2  27062  ftalem3  27063  muval1  27121  dvdssqf  27126  sqff1o  27170  chtub  27200  bposlem3  27274  lgsne0  27323  gausslemma2dlem1a  27353  gausslemma2dlem2  27355  lgseisenlem1  27363  lgseisenlem2  27364  lgsquadlem1  27368  lgsquadlem2  27369  lgsquadlem3  27370  lgsquad2lem1  27372  lgsquad2lem2  27373  dchrisum0lem1  27504  pntlem3  27597  negbdaylem  28073  mulsproplem5  28137  mulsproplem8  28140  bdayons  28293  z12bdaylem1  28487  upgrewlkle2  29700  pthdlem1  29859  crctcshwlkn0lem3  29905  ex-natded5.8-2  30509  nmoub3i  30869  ubthlem1  30966  ubthlem2  30967  shsel1  31417  nmopub2tALT  32005  nmfnleub2  32022  lnconi  32129  eulerpartlemb  34559  r1elcl  35286  dfon2lem4  36019  btwncomim  36248  nn0prpwlem  36557  cgsex2gd  37504  ltflcei  37982  poimirlem9  38003  poimirlem18  38012  poimirlem21  38015  poimirlem22  38016  poimirlem24  38018  poimirlem29  38023  heicant  38029  mbfresfi  38040  itg2addnclem2  38046  itg2addnclem3  38047  incsequz  38122  heibor1lem  38183  atlelt  39937  1cvratex  39972  dalem3  40163  linepsubN  40251  pmapsub  40267  2llnma3r  40287  cdlemblem  40292  pmapjoin  40351  atmod1i1  40356  atmod1i2  40358  llnmod1i2  40359  lhpmcvr4N  40525  4atexlemnclw  40569  cdlemd3  40699  cdleme3g  40733  cdleme3h  40734  cdleme7d  40745  cdleme7ga  40747  cdleme21c  40826  cdleme35fnpq  40948  cdleme35f  40953  cdlemf1  41060  cdlemg4  41116  cdlemg6c  41119  cdlemg27a  41191  cdlemg33b0  41200  cdlemg33a  41205  cdlemk3  41332  dia2dimlem1  41563  dvheveccl  41611  dihord6apre  41755  dihord6b  41759  coprmdvdsb  43437  harval3  43989  monoordxrv  45931  stoweid  46513  smonoord  47847  iccpartgt  47909  goldbachthlem2  48031  lighneallem2  48091  tgoldbach  48315  nn0sumltlt  48848  dignn0flhalflem1  49113