Theorem mpan2d 677

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  mpand  678  mpan2i  680  ralxfrd  5090  ralxfrd2  5094  sotri3  5750  oeordi  7913  xpfi  8479  alephle  9203  axdc3lem4  9569  dedekindle  10495  addlsub  10741  letrp1  11159  ledivp1  11219  peano2uz2  11750  uzind  11754  xrre  12237  xrre2  12238  xrltmin  12250  xrlemin  12252  lemaxle  12263  xralrple  12273  xlemul1a  12355  xrinfmsslem  12375  flge  12849  flflp1  12851  fsequb  13017  seqcl2  13061  monoord  13073  facwordi  13315  facavg  13327  sqrlem6  14230  leabs  14281  caubnd  14340  limsupgre  14454  limsupbnd2  14456  lo1bdd2  14497  lo1bddrp  14498  o1lo1  14510  o1rlimmul  14591  lo1mul  14600  isercolllem2  14638  climcndslem1  14822  climcndslem2  14823  ruclem3  15201  ruclem9  15206  ruclem12  15209  dvdsmultr1  15261  ltoddhalfle  15324  divalglem0  15355  dvdsgcdb  15500  dfgcd2  15501  coprmgcdb  15600  coprmdvds2  15605  exprmfct  15652  prmdvdsfz  15653  prmfac1  15667  rpexp  15668  eulerthlem2  15723  pcpremul  15784  pcdvdsb  15809  pcprmpw2  15822  pockthlem  15845  prmreclem3  15858  4sqlem11  15895  vdwnnlem3  15937  meetle  17252  latjlej1  17289  latnlej2  17295  clatleglb  17350  mndodconglem  18180  efgsrel  18367  ablfac1b  18690  pgpfac1lem1  18694  lbsextlem2  19387  chfacfscmul0  20896  chfacfpmmul0  20900  lmcls  21340  ufileu  21956  ufilcmp  22069  cnpfcf  22078  tsmsxp  22191  prdsbl  22529  reconnlem2  22863  evth  22991  ivthlem2  23455  ivthlem3  23456  ovollb2lem  23491  ovoliunlem2  23506  ovolicc2lem3  23522  ismbf3d  23657  itg2seq  23745  itg2monolem1  23753  dvcnvrelem1  24016  itgsubst  24048  plypf1  24204  coeaddlem  24241  coemullem  24242  ulmcau  24385  abelth  24431  wilth  25033  ftalem2  25036  ftalem3  25037  muval1  25095  dvdssqf  25100  sqff1o  25144  chtub  25173  bposlem3  25247  lgsne0  25296  gausslemma2dlem1a  25326  gausslemma2dlem2  25328  lgseisenlem1  25336  lgseisenlem2  25337  lgsquadlem1  25341  lgsquadlem2  25342  lgsquadlem3  25343  lgsquad2lem1  25345  lgsquad2lem2  25346  dchrisum0lem1  25441  pntlem3  25534  upgrewlkle2  26752  pthdlem1  26912  crctcshwlkn0lem3  26955  ex-natded5.8-2  27624  nmoub3i  27978  ubthlem1  28076  ubthlem2  28077  shsel1  28530  nmopub2tALT  29118  nmfnleub2  29135  lnconi  29242  eulerpartlemb  30777  dfon2lem4  32032  btwncomim  32462  nn0prpwlem  32659  ltflcei  33728  poimirlem9  33749  poimirlem18  33758  poimirlem21  33761  poimirlem22  33762  poimirlem24  33764  poimirlem29  33769  heicant  33775  mbfresfi  33786  itg2addnclem2  33792  itg2addnclem3  33793  incsequz  33873  heibor1lem  33937  atlelt  35236  1cvratex  35271  dalem3  35462  linepsubN  35550  pmapsub  35566  2llnma3r  35586  cdlemblem  35591  pmapjoin  35650  atmod1i1  35655  atmod1i2  35657  llnmod1i2  35658  lhpmcvr4N  35824  4atexlemnclw  35868  cdlemd3  35998  cdleme3g  36032  cdleme3h  36033  cdleme7d  36044  cdleme7ga  36046  cdleme21c  36125  cdleme35fnpq  36247  cdleme35f  36252  cdlemf1  36359  cdlemg4  36415  cdlemg6c  36418  cdlemg27a  36490  cdlemg33b0  36499  cdlemg33a  36504  cdlemk3  36631  dia2dimlem1  36862  dvheveccl  36910  dihord6apre  37054  dihord6b  37058  coprmdvdsb  38070  monoordxrv  40208  stoweid  40776  smonoord  41933  iccpartgt  41955  goldbachthlem2  42050  lighneallem2  42115  tgoldbach  42297  nn0sumltlt  42713  dignn0flhalflem1  42994