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  5375  ralxfrd2  5379  sotri3  6116  predtrss  6308  oeordi  8593  coflton  8677  cofon1  8678  cofon2  8679  xpfiOLD  9325  ttrclss  9726  alephle  10094  axdc3lem4  10459  dedekindle  11391  addlsub  11645  letrp1  12077  ledivp1  12136  peano2uz2  12673  uzind  12677  xrre  13177  xrre2  13178  xrltmin  13190  xrlemin  13192  lemaxle  13203  xralrple  13213  xlemul1a  13296  xrinfmsslem  13316  flge  13811  flflp1  13813  fsequb  13982  seqcl2  14027  monoord  14039  facwordi  14295  facavg  14307  01sqrexlem6  15253  leabs  15305  caubnd  15364  limsupgre  15484  limsupbnd2  15486  lo1bdd2  15527  lo1bddrp  15528  o1lo1  15540  o1rlimmul  15622  lo1mul  15631  isercolllem2  15669  climcndslem1  15852  climcndslem2  15853  ruclem3  16236  ruclem9  16241  ruclem12  16244  dvdsmultr1  16300  ltoddhalfle  16365  divalglem0  16397  dvdsgcdb  16549  dfgcd2  16550  coprmgcdb  16653  coprmdvds2  16658  exprmfct  16708  prmdvdsfz  16709  prmfac1  16724  rpexp  16726  eulerthlem2  16786  pcpremul  16848  pcdvdsb  16874  pcprmpw2  16887  pockthlem  16910  prmreclem3  16923  4sqlem11  16960  vdwnnlem3  17002  meetle  18395  latjlej1  18448  latnlej2  18454  clatleglb  18513  mndodconglem  19507  efgsrel  19700  ablfac1b  20038  pgpfac1lem1  20042  lbsextlem2  21105  psdmul  22089  chfacfscmul0  22781  chfacfpmmul0  22785  lmcls  23225  ufileu  23842  ufilcmp  23955  cnpfcf  23964  tsmsxp  24078  prdsbl  24415  reconnlem2  24752  evth  24894  ivthlem2  25390  ivthlem3  25391  ovollb2lem  25426  ovoliunlem2  25441  ovolicc2lem3  25457  ismbf3d  25592  itg2seq  25680  itg2monolem1  25688  dvcnvrelem1  25959  itgsubst  25993  plypf1  26154  coeaddlem  26191  coemullem  26192  ulmcau  26341  abelth  26388  wilth  27017  ftalem2  27020  ftalem3  27021  muval1  27079  dvdssqf  27084  sqff1o  27128  chtub  27159  bposlem3  27233  lgsne0  27282  gausslemma2dlem1a  27312  gausslemma2dlem2  27314  lgseisenlem1  27322  lgseisenlem2  27323  lgsquadlem1  27327  lgsquadlem2  27328  lgsquadlem3  27329  lgsquad2lem1  27331  lgsquad2lem2  27332  dchrisum0lem1  27463  pntlem3  27556  negsbdaylem  27991  mulsproplem5  28049  mulsproplem8  28052  upgrewlkle2  29518  pthdlem1  29680  crctcshwlkn0lem3  29726  ex-natded5.8-2  30327  nmoub3i  30686  ubthlem1  30783  ubthlem2  30784  shsel1  31234  nmopub2tALT  31822  nmfnleub2  31839  lnconi  31946  eulerpartlemb  34308  dfon2lem4  35725  btwncomim  35952  nn0prpwlem  36261  ltflcei  37553  poimirlem9  37574  poimirlem18  37583  poimirlem21  37586  poimirlem22  37587  poimirlem24  37589  poimirlem29  37594  heicant  37600  mbfresfi  37611  itg2addnclem2  37617  itg2addnclem3  37618  incsequz  37693  heibor1lem  37754  atlelt  39378  1cvratex  39413  dalem3  39604  linepsubN  39692  pmapsub  39708  2llnma3r  39728  cdlemblem  39733  pmapjoin  39792  atmod1i1  39797  atmod1i2  39799  llnmod1i2  39800  lhpmcvr4N  39966  4atexlemnclw  40010  cdlemd3  40140  cdleme3g  40174  cdleme3h  40175  cdleme7d  40186  cdleme7ga  40188  cdleme21c  40267  cdleme35fnpq  40389  cdleme35f  40394  cdlemf1  40501  cdlemg4  40557  cdlemg6c  40560  cdlemg27a  40632  cdlemg33b0  40641  cdlemg33a  40646  cdlemk3  40773  dia2dimlem1  41004  dvheveccl  41052  dihord6apre  41196  dihord6b  41200  coprmdvdsb  42934  harval3  43487  monoordxrv  45436  stoweid  46022  smonoord  47303  iccpartgt  47359  goldbachthlem2  47478  lighneallem2  47538  tgoldbach  47749  nn0sumltlt  48211  dignn0flhalflem1  48481