Theorem mpan2d 690

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 206  df-an 396

This theorem is referenced by:  mpand  691  mpan2i  693  ralxfrd  5326  ralxfrd2  5330  sotri3  6024  predtrss  6214  oeordi  8380  xpfi  9015  alephle  9775  axdc3lem4  10140  dedekindle  11069  addlsub  11321  letrp1  11749  ledivp1  11807  peano2uz2  12338  uzind  12342  xrre  12832  xrre2  12833  xrltmin  12845  xrlemin  12847  lemaxle  12858  xralrple  12868  xlemul1a  12951  xrinfmsslem  12971  flge  13453  flflp1  13455  fsequb  13623  seqcl2  13669  monoord  13681  facwordi  13931  facavg  13943  sqrlem6  14887  leabs  14939  caubnd  14998  limsupgre  15118  limsupbnd2  15120  lo1bdd2  15161  lo1bddrp  15162  o1lo1  15174  o1rlimmul  15256  lo1mul  15265  isercolllem2  15305  climcndslem1  15489  climcndslem2  15490  ruclem3  15870  ruclem9  15875  ruclem12  15878  dvdsmultr1  15933  ltoddhalfle  15998  divalglem0  16030  dvdsgcdb  16181  dfgcd2  16182  coprmgcdb  16282  coprmdvds2  16287  exprmfct  16337  prmdvdsfz  16338  prmfac1  16354  rpexp  16355  eulerthlem2  16411  pcpremul  16472  pcdvdsb  16498  pcprmpw2  16511  pockthlem  16534  prmreclem3  16547  4sqlem11  16584  vdwnnlem3  16626  meetle  18033  latjlej1  18086  latnlej2  18092  clatleglb  18151  mndodconglem  19064  efgsrel  19255  ablfac1b  19588  pgpfac1lem1  19592  lbsextlem2  20336  chfacfscmul0  21915  chfacfpmmul0  21919  lmcls  22361  ufileu  22978  ufilcmp  23091  cnpfcf  23100  tsmsxp  23214  prdsbl  23553  reconnlem2  23896  evth  24028  ivthlem2  24521  ivthlem3  24522  ovollb2lem  24557  ovoliunlem2  24572  ovolicc2lem3  24588  ismbf3d  24723  itg2seq  24812  itg2monolem1  24820  dvcnvrelem1  25086  itgsubst  25118  plypf1  25278  coeaddlem  25315  coemullem  25316  ulmcau  25459  abelth  25505  wilth  26125  ftalem2  26128  ftalem3  26129  muval1  26187  dvdssqf  26192  sqff1o  26236  chtub  26265  bposlem3  26339  lgsne0  26388  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  lgseisenlem1  26428  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  lgsquadlem3  26435  lgsquad2lem1  26437  lgsquad2lem2  26438  dchrisum0lem1  26569  pntlem3  26662  upgrewlkle2  27876  pthdlem1  28035  crctcshwlkn0lem3  28078  ex-natded5.8-2  28679  nmoub3i  29036  ubthlem1  29133  ubthlem2  29134  shsel1  29584  nmopub2tALT  30172  nmfnleub2  30189  lnconi  30296  eulerpartlemb  32235  dfon2lem4  33668  ttrclss  33706  btwncomim  34242  nn0prpwlem  34438  ltflcei  35692  poimirlem9  35713  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  poimirlem24  35728  poimirlem29  35733  heicant  35739  mbfresfi  35750  itg2addnclem2  35756  itg2addnclem3  35757  incsequz  35833  heibor1lem  35894  atlelt  37379  1cvratex  37414  dalem3  37605  linepsubN  37693  pmapsub  37709  2llnma3r  37729  cdlemblem  37734  pmapjoin  37793  atmod1i1  37798  atmod1i2  37800  llnmod1i2  37801  lhpmcvr4N  37967  4atexlemnclw  38011  cdlemd3  38141  cdleme3g  38175  cdleme3h  38176  cdleme7d  38187  cdleme7ga  38189  cdleme21c  38268  cdleme35fnpq  38390  cdleme35f  38395  cdlemf1  38502  cdlemg4  38558  cdlemg6c  38561  cdlemg27a  38633  cdlemg33b0  38642  cdlemg33a  38647  cdlemk3  38774  dia2dimlem1  39005  dvheveccl  39053  dihord6apre  39197  dihord6b  39201  coprmdvdsb  40723  harval3  41041  monoordxrv  42912  stoweid  43494  smonoord  44711  iccpartgt  44767  goldbachthlem2  44886  lighneallem2  44946  tgoldbach  45157  nn0sumltlt  45574  dignn0flhalflem1  45849