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  5378  ralxfrd2  5382  sotri3  6119  predtrss  6311  oeordi  8597  coflton  8681  cofon1  8682  cofon2  8683  xpfiOLD  9329  ttrclss  9732  alephle  10100  axdc3lem4  10465  dedekindle  11397  addlsub  11651  letrp1  12083  ledivp1  12142  peano2uz2  12679  uzind  12683  xrre  13183  xrre2  13184  xrltmin  13196  xrlemin  13198  lemaxle  13209  xralrple  13219  xlemul1a  13302  xrinfmsslem  13322  flge  13820  flflp1  13822  fsequb  13991  seqcl2  14036  monoord  14048  facwordi  14305  facavg  14317  01sqrexlem6  15264  leabs  15316  caubnd  15375  limsupgre  15495  limsupbnd2  15497  lo1bdd2  15538  lo1bddrp  15539  o1lo1  15551  o1rlimmul  15633  lo1mul  15642  isercolllem2  15680  climcndslem1  15863  climcndslem2  15864  ruclem3  16249  ruclem9  16254  ruclem12  16257  dvdsmultr1  16313  ltoddhalfle  16378  divalglem0  16410  dvdsgcdb  16562  dfgcd2  16563  coprmgcdb  16666  coprmdvds2  16671  exprmfct  16721  prmdvdsfz  16722  prmfac1  16737  rpexp  16739  eulerthlem2  16799  pcpremul  16861  pcdvdsb  16887  pcprmpw2  16900  pockthlem  16923  prmreclem3  16936  4sqlem11  16973  vdwnnlem3  17015  meetle  18408  latjlej1  18461  latnlej2  18467  clatleglb  18526  mndodconglem  19520  efgsrel  19713  ablfac1b  20051  pgpfac1lem1  20055  lbsextlem2  21118  psdmul  22102  chfacfscmul0  22794  chfacfpmmul0  22798  lmcls  23238  ufileu  23855  ufilcmp  23968  cnpfcf  23977  tsmsxp  24091  prdsbl  24428  reconnlem2  24765  evth  24907  ivthlem2  25403  ivthlem3  25404  ovollb2lem  25439  ovoliunlem2  25454  ovolicc2lem3  25470  ismbf3d  25605  itg2seq  25693  itg2monolem1  25701  dvcnvrelem1  25972  itgsubst  26006  plypf1  26167  coeaddlem  26204  coemullem  26205  ulmcau  26354  abelth  26401  wilth  27031  ftalem2  27034  ftalem3  27035  muval1  27093  dvdssqf  27098  sqff1o  27142  chtub  27173  bposlem3  27247  lgsne0  27296  gausslemma2dlem1a  27326  gausslemma2dlem2  27328  lgseisenlem1  27336  lgseisenlem2  27337  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  lgsquad2lem1  27345  lgsquad2lem2  27346  dchrisum0lem1  27477  pntlem3  27570  negsbdaylem  28005  mulsproplem5  28063  mulsproplem8  28066  upgrewlkle2  29532  pthdlem1  29694  crctcshwlkn0lem3  29740  ex-natded5.8-2  30341  nmoub3i  30700  ubthlem1  30797  ubthlem2  30798  shsel1  31248  nmopub2tALT  31836  nmfnleub2  31853  lnconi  31960  eulerpartlemb  34346  dfon2lem4  35750  btwncomim  35977  nn0prpwlem  36286  ltflcei  37578  poimirlem9  37599  poimirlem18  37608  poimirlem21  37611  poimirlem22  37612  poimirlem24  37614  poimirlem29  37619  heicant  37625  mbfresfi  37636  itg2addnclem2  37642  itg2addnclem3  37643  incsequz  37718  heibor1lem  37779  atlelt  39403  1cvratex  39438  dalem3  39629  linepsubN  39717  pmapsub  39733  2llnma3r  39753  cdlemblem  39758  pmapjoin  39817  atmod1i1  39822  atmod1i2  39824  llnmod1i2  39825  lhpmcvr4N  39991  4atexlemnclw  40035  cdlemd3  40165  cdleme3g  40199  cdleme3h  40200  cdleme7d  40211  cdleme7ga  40213  cdleme21c  40292  cdleme35fnpq  40414  cdleme35f  40419  cdlemf1  40526  cdlemg4  40582  cdlemg6c  40585  cdlemg27a  40657  cdlemg33b0  40666  cdlemg33a  40671  cdlemk3  40798  dia2dimlem1  41029  dvheveccl  41077  dihord6apre  41221  dihord6b  41225  coprmdvdsb  42956  harval3  43509  monoordxrv  45456  stoweid  46040  smonoord  47333  iccpartgt  47389  goldbachthlem2  47508  lighneallem2  47568  tgoldbach  47779  nn0sumltlt  48273  dignn0flhalflem1  48543