Theorem mpan2d 706

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpand  707  mpan2i  709  ralxfrd  5381  ralxfrd2  5385  sotri3  6132  predtrss  6325  oeordi  8574  coflton  8658  cofon1  8659  cofon2  8660  ttrclss  9690  alephle  10073  axdc3lem4  10438  dedekindle  11375  addlsub  11631  letrp1  12060  ledivp1  12118  peano2uz2  12685  uzind  12689  xrre  13196  xrre2  13197  xrltmin  13209  xrlemin  13211  lemaxle  13222  xralrple  13232  xlemul1a  13315  xrinfmsslem  13335  flge  13840  flflp1  13842  fsequb  14013  seqcl2  14058  monoord  14070  facwordi  14327  facavg  14339  01sqrexlem6  15300  leabs  15352  caubnd  15412  limsupgre  15534  limsupbnd2  15536  lo1bdd2  15577  lo1bddrp  15578  o1lo1  15590  o1rlimmul  15672  lo1mul  15681  isercolllem2  15719  climcndslem1  15905  climcndslem2  15906  ruclem3  16290  ruclem9  16295  ruclem12  16298  dvdsmultr1  16355  ltoddhalfle  16420  divalglem0  16452  dvdsgcdb  16604  dfgcd2  16605  coprmgcdb  16708  coprmdvds2  16713  exprmfct  16764  prmdvdsfz  16765  prmfac1  16780  rpexp  16782  eulerthlem2  16842  pcpremul  16904  pcdvdsb  16930  pcprmpw2  16943  pockthlem  16966  prmreclem3  16979  4sqlem11  17016  vdwnnlem3  17058  meetle  18455  latjlej1  18510  latnlej2  18516  clatleglb  18575  mndodconglem  19612  efgsrel  19805  ablfac1b  20143  pgpfac1lem1  20147  lbsextlem2  21264  psdmul  22310  chfacfscmul0  22996  chfacfpmmul0  23000  lmcls  23440  ufileu  24057  ufilcmp  24170  cnpfcf  24179  tsmsxp  24293  prdsbl  24629  reconnlem2  24966  evth  25099  ivthlem2  25592  ivthlem3  25593  ovollb2lem  25628  ovoliunlem2  25643  ovolicc2lem3  25659  ismbf3d  25794  itg2seq  25882  itg2monolem1  25890  dvcnvrelem1  26157  itgsubst  26189  plypf1  26350  coeaddlem  26387  coemullem  26388  ulmcau  26536  abelth  26582  wilth  27213  ftalem2  27216  ftalem3  27217  muval1  27275  dvdssqf  27280  sqff1o  27324  chtub  27354  bposlem3  27428  lgsne0  27477  gausslemma2dlem1a  27507  gausslemma2dlem2  27509  lgseisenlem1  27517  lgseisenlem2  27518  lgsquadlem1  27522  lgsquadlem2  27523  lgsquadlem3  27524  lgsquad2lem1  27526  lgsquad2lem2  27527  dchrisum0lem1  27658  pntlem3  27751  negbdaylem  28227  mulsproplem5  28291  mulsproplem8  28294  bdayons  28447  z12bdaylem1  28641  upgrewlkle2  29934  pthdlem1  30093  crctcshwlkn0lem3  30139  ex-natded5.8-2  30743  nmoub3i  31103  ubthlem1  31200  ubthlem2  31201  shsel1  31651  nmopub2tALT  32239  nmfnleub2  32256  lnconi  32363  eulerpartlemb  34736  r1elcl  35469  karddom  35552  kardsdom  35553  dfon2lem4  36254  btwncomim  36483  ltnmul  36671  nn0prpwlem  36811  cgsex2gd  37759  ltflcei  38237  poimirlem9  38258  poimirlem18  38267  poimirlem21  38270  poimirlem22  38271  poimirlem24  38273  poimirlem29  38278  heicant  38284  mbfresfi  38295  itg2addnclem2  38301  itg2addnclem3  38302  incsequz  38377  heibor1lem  38438  atlelt  40190  1cvratex  40225  dalem3  40416  linepsubN  40504  pmapsub  40520  2llnma3r  40540  cdlemblem  40545  pmapjoin  40604  atmod1i1  40609  atmod1i2  40611  llnmod1i2  40612  lhpmcvr4N  40778  4atexlemnclw  40822  cdlemd3  40952  cdleme3g  40986  cdleme3h  40987  cdleme7d  40998  cdleme7ga  41000  cdleme21c  41079  cdleme35fnpq  41201  cdleme35f  41206  cdlemf1  41313  cdlemg4  41369  cdlemg6c  41372  cdlemg27a  41444  cdlemg33b0  41453  cdlemg33a  41458  cdlemk3  41585  dia2dimlem1  41816  dvheveccl  41864  dihord6apre  42008  dihord6b  42012  coprmdvdsb  43692  harval3  44244  monoordxrv  46175  stoweid  46757  smonoord  48091  iccpartgt  48153  goldbachthlem2  48275  lighneallem2  48335  tgoldbach  48559  nn0sumltlt  49107  dignn0flhalflem1  49372