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  5350  ralxfrd2  5354  sotri3  6093  predtrss  6286  oeordi  8523  coflton  8607  cofon1  8608  cofon2  8609  ttrclss  9641  alephle  10010  axdc3lem4  10375  dedekindle  11310  addlsub  11566  letrp1  11999  ledivp1  12058  peano2uz2  12617  uzind  12621  xrre  13121  xrre2  13122  xrltmin  13134  xrlemin  13136  lemaxle  13147  xralrple  13157  xlemul1a  13240  xrinfmsslem  13260  flge  13764  flflp1  13766  fsequb  13937  seqcl2  13982  monoord  13994  facwordi  14251  facavg  14263  01sqrexlem6  15209  leabs  15261  caubnd  15321  limsupgre  15443  limsupbnd2  15445  lo1bdd2  15486  lo1bddrp  15487  o1lo1  15499  o1rlimmul  15581  lo1mul  15590  isercolllem2  15628  climcndslem1  15814  climcndslem2  15815  ruclem3  16200  ruclem9  16205  ruclem12  16208  dvdsmultr1  16265  ltoddhalfle  16330  divalglem0  16362  dvdsgcdb  16514  dfgcd2  16515  coprmgcdb  16618  coprmdvds2  16623  exprmfct  16674  prmdvdsfz  16675  prmfac1  16690  rpexp  16692  eulerthlem2  16752  pcpremul  16814  pcdvdsb  16840  pcprmpw2  16853  pockthlem  16876  prmreclem3  16889  4sqlem11  16926  vdwnnlem3  16968  meetle  18364  latjlej1  18419  latnlej2  18425  clatleglb  18484  mndodconglem  19516  efgsrel  19709  ablfac1b  20047  pgpfac1lem1  20051  lbsextlem2  21157  psdmul  22132  chfacfscmul0  22823  chfacfpmmul0  22827  lmcls  23267  ufileu  23884  ufilcmp  23997  cnpfcf  24006  tsmsxp  24120  prdsbl  24456  reconnlem2  24793  evth  24926  ivthlem2  25419  ivthlem3  25420  ovollb2lem  25455  ovoliunlem2  25470  ovolicc2lem3  25486  ismbf3d  25621  itg2seq  25709  itg2monolem1  25717  dvcnvrelem1  25984  itgsubst  26016  plypf1  26177  coeaddlem  26214  coemullem  26215  ulmcau  26360  abelth  26406  wilth  27034  ftalem2  27037  ftalem3  27038  muval1  27096  dvdssqf  27101  sqff1o  27145  chtub  27175  bposlem3  27249  lgsne0  27298  gausslemma2dlem1a  27328  gausslemma2dlem2  27330  lgseisenlem1  27338  lgseisenlem2  27339  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  lgsquad2lem1  27347  lgsquad2lem2  27348  dchrisum0lem1  27479  pntlem3  27572  negbdaylem  28048  mulsproplem5  28112  mulsproplem8  28115  bdayons  28268  z12bdaylem1  28462  upgrewlkle2  29675  pthdlem1  29834  crctcshwlkn0lem3  29880  ex-natded5.8-2  30484  nmoub3i  30844  ubthlem1  30941  ubthlem2  30942  shsel1  31392  nmopub2tALT  31980  nmfnleub2  31997  lnconi  32104  eulerpartlemb  34512  r1elcl  35241  dfon2lem4  35966  btwncomim  36195  nn0prpwlem  36504  cgsex2gd  37451  ltflcei  37929  poimirlem9  37950  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem24  37965  poimirlem29  37970  heicant  37976  mbfresfi  37987  itg2addnclem2  37993  itg2addnclem3  37994  incsequz  38069  heibor1lem  38130  atlelt  39884  1cvratex  39919  dalem3  40110  linepsubN  40198  pmapsub  40214  2llnma3r  40234  cdlemblem  40239  pmapjoin  40298  atmod1i1  40303  atmod1i2  40305  llnmod1i2  40306  lhpmcvr4N  40472  4atexlemnclw  40516  cdlemd3  40646  cdleme3g  40680  cdleme3h  40681  cdleme7d  40692  cdleme7ga  40694  cdleme21c  40773  cdleme35fnpq  40895  cdleme35f  40900  cdlemf1  41007  cdlemg4  41063  cdlemg6c  41066  cdlemg27a  41138  cdlemg33b0  41147  cdlemg33a  41152  cdlemk3  41279  dia2dimlem1  41510  dvheveccl  41558  dihord6apre  41702  dihord6b  41706  coprmdvdsb  43413  harval3  43965  monoordxrv  45909  stoweid  46491  smonoord  47825  iccpartgt  47887  goldbachthlem2  48009  lighneallem2  48069  tgoldbach  48293  nn0sumltlt  48826  dignn0flhalflem1  49091