Theorem mpan2d 707

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpand  708  mpan2i  710  ralxfrd  5370  ralxfrd2  5374  sotri3  6122  predtrss  6318  oeordi  8580  coflton  8664  cofon1  8665  cofon2  8666  ttrclss  9705  alephle  10148  axdc3lem4  10512  dedekindle  11455  addlsub  11713  letrp1  12142  ledivp1  12200  peano2uz2  12768  uzind  12772  xrre  13280  xrre2  13281  xrltmin  13293  xrlemin  13295  lemaxle  13306  xralrple  13316  xlemul1a  13399  xrinfmsslem  13419  flge  13925  flflp1  13927  fsequb  14098  seqcl2  14143  monoord  14155  facwordi  14413  facavg  14425  01sqrexlem6  15394  leabs  15446  caubnd  15506  limsupgre  15628  limsupbnd2  15630  lo1bdd2  15671  lo1bddrp  15672  o1lo1  15684  o1rlimmul  15766  lo1mul  15775  isercolllem2  15813  climcndslem1  15998  climcndslem2  15999  ruclem3  16381  ruclem9  16386  ruclem12  16389  dvdsmultr1  16446  ltoddhalfle  16511  divalglem0  16543  dvdsgcdb  16698  dfgcd2  16699  coprmgcdb  16804  coprmdvds2  16809  exprmfct  16860  prmdvdsfz  16861  prmfac1  16876  rpexp  16878  eulerthlem2  16939  pcpremul  17001  pcdvdsb  17027  pcprmpw2  17040  pockthlem  17063  prmreclem3  17076  4sqlem11  17113  vdwnnlem3  17155  meetle  18552  latjlej1  18607  latnlej2  18613  clatleglb  18672  mndodconglem  19735  efgsrel  19928  ablfac1b  20266  pgpfac1lem1  20270  lbsextlem2  21417  psdmul  22467  chfacfscmul0  23156  chfacfpmmul0  23160  lmcls  23600  ufileu  24218  ufilcmp  24331  cnpfcf  24340  tsmsxp  24454  prdsbl  24790  reconnlem2  25127  evth  25260  ivthlem2  25753  ivthlem3  25754  ovollb2lem  25789  ovoliunlem2  25804  ovolicc2lem3  25820  ismbf3d  25955  itg2seq  26043  itg2monolem1  26051  dvcnvrelem1  26317  itgsubst  26349  plypf1  26511  coeaddlem  26548  coemullem  26549  ulmcau  26704  abelth  26750  wilth  27380  ftalem2  27383  ftalem3  27384  muval1  27442  dvdssqf  27447  sqff1o  27491  chtub  27521  bposlem3  27595  lgsne0  27644  gausslemma2dlem1a  27674  gausslemma2dlem2  27676  lgseisenlem1  27684  lgseisenlem2  27685  lgsquadlem1  27689  lgsquadlem2  27690  lgsquadlem3  27691  lgsquad2lem1  27693  lgsquad2lem2  27694  dchrisum0lem1  27825  pntlem3  27918  negbdaylem  28424  mulsproplem5  28488  mulsproplem8  28491  bdayons  28644  z12bdaylem1  28838  upgrewlkle2  30169  pthdlem1  30334  crctcshwlkn0lem3  30383  ex-natded5.8-2  30997  nmoub3i  31357  ubthlem1  31454  ubthlem2  31455  shsel1  31905  nmopub2tALT  32493  nmfnleub2  32510  lnconi  32617  eulerpartlemb  34983  karddom  35802  kardsdom  35803  dfon2lem4  36518  btwncomim  36748  ltnmul  36935  nn0prpwlem  37080  cgsex2gd  38026  ltflcei  38499  poimirlem9  38515  poimirlem18  38524  poimirlem21  38527  poimirlem22  38528  poimirlem24  38530  poimirlem29  38535  heicant  38541  mbfresfi  38552  itg2addnclem2  38558  itg2addnclem3  38559  incsequz  38650  heibor1lem  38711  atlelt  40463  1cvratex  40498  dalem3  40689  linepsubN  40777  pmapsub  40793  2llnma3r  40813  cdlemblem  40818  pmapjoin  40877  atmod1i1  40882  atmod1i2  40884  llnmod1i2  40885  lhpmcvr4N  41051  4atexlemnclw  41095  cdlemd3  41225  cdleme3g  41259  cdleme3h  41260  cdleme7d  41271  cdleme7ga  41273  cdleme21c  41352  cdleme35fnpq  41474  cdleme35f  41479  cdlemf1  41586  cdlemg4  41642  cdlemg6c  41645  cdlemg27a  41717  cdlemg33b0  41726  cdlemg33a  41731  cdlemk3  41858  dia2dimlem1  42089  dvheveccl  42137  dihord6apre  42281  dihord6b  42285  coprmdvdsb  43945  harval3  44497  monoordxrv  46435  stoweid  47017  smonoord  48391  iccpartgt  48453  goldbachthlem2  48575  lighneallem2  48635  tgoldbach  48859  nn0sumltlt  49406  dignn0flhalflem1  49671