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  5346  ralxfrd2  5350  sotri3  6077  predtrss  6269  oeordi  8502  coflton  8586  cofon1  8587  cofon2  8588  ttrclss  9610  alephle  9976  axdc3lem4  10341  dedekindle  11274  addlsub  11530  letrp1  11962  ledivp1  12021  peano2uz2  12558  uzind  12562  xrre  13065  xrre2  13066  xrltmin  13078  xrlemin  13080  lemaxle  13091  xralrple  13101  xlemul1a  13184  xrinfmsslem  13204  flge  13706  flflp1  13708  fsequb  13879  seqcl2  13924  monoord  13936  facwordi  14193  facavg  14205  01sqrexlem6  15151  leabs  15203  caubnd  15263  limsupgre  15385  limsupbnd2  15387  lo1bdd2  15428  lo1bddrp  15429  o1lo1  15441  o1rlimmul  15523  lo1mul  15532  isercolllem2  15570  climcndslem1  15753  climcndslem2  15754  ruclem3  16139  ruclem9  16144  ruclem12  16147  dvdsmultr1  16204  ltoddhalfle  16269  divalglem0  16301  dvdsgcdb  16453  dfgcd2  16454  coprmgcdb  16557  coprmdvds2  16562  exprmfct  16612  prmdvdsfz  16613  prmfac1  16628  rpexp  16630  eulerthlem2  16690  pcpremul  16752  pcdvdsb  16778  pcprmpw2  16791  pockthlem  16814  prmreclem3  16827  4sqlem11  16864  vdwnnlem3  16906  meetle  18301  latjlej1  18356  latnlej2  18362  clatleglb  18421  mndodconglem  19451  efgsrel  19644  ablfac1b  19982  pgpfac1lem1  19986  lbsextlem2  21094  psdmul  22079  chfacfscmul0  22771  chfacfpmmul0  22775  lmcls  23215  ufileu  23832  ufilcmp  23945  cnpfcf  23954  tsmsxp  24068  prdsbl  24404  reconnlem2  24741  evth  24883  ivthlem2  25378  ivthlem3  25379  ovollb2lem  25414  ovoliunlem2  25429  ovolicc2lem3  25445  ismbf3d  25580  itg2seq  25668  itg2monolem1  25676  dvcnvrelem1  25947  itgsubst  25981  plypf1  26142  coeaddlem  26179  coemullem  26180  ulmcau  26329  abelth  26376  wilth  27006  ftalem2  27009  ftalem3  27010  muval1  27068  dvdssqf  27073  sqff1o  27117  chtub  27148  bposlem3  27222  lgsne0  27271  gausslemma2dlem1a  27301  gausslemma2dlem2  27303  lgseisenlem1  27311  lgseisenlem2  27312  lgsquadlem1  27316  lgsquadlem2  27317  lgsquadlem3  27318  lgsquad2lem1  27320  lgsquad2lem2  27321  dchrisum0lem1  27452  pntlem3  27545  negsbdaylem  27996  mulsproplem5  28057  mulsproplem8  28060  bdayon  28207  upgrewlkle2  29583  pthdlem1  29742  crctcshwlkn0lem3  29788  ex-natded5.8-2  30389  nmoub3i  30748  ubthlem1  30845  ubthlem2  30846  shsel1  31296  nmopub2tALT  31884  nmfnleub2  31901  lnconi  32008  eulerpartlemb  34376  r1elcl  35102  dfon2lem4  35819  btwncomim  36046  nn0prpwlem  36355  ltflcei  37647  poimirlem9  37668  poimirlem18  37677  poimirlem21  37680  poimirlem22  37681  poimirlem24  37683  poimirlem29  37688  heicant  37694  mbfresfi  37705  itg2addnclem2  37711  itg2addnclem3  37712  incsequz  37787  heibor1lem  37848  atlelt  39476  1cvratex  39511  dalem3  39702  linepsubN  39790  pmapsub  39806  2llnma3r  39826  cdlemblem  39831  pmapjoin  39890  atmod1i1  39895  atmod1i2  39897  llnmod1i2  39898  lhpmcvr4N  40064  4atexlemnclw  40108  cdlemd3  40238  cdleme3g  40272  cdleme3h  40273  cdleme7d  40284  cdleme7ga  40286  cdleme21c  40365  cdleme35fnpq  40487  cdleme35f  40492  cdlemf1  40599  cdlemg4  40655  cdlemg6c  40658  cdlemg27a  40730  cdlemg33b0  40739  cdlemg33a  40744  cdlemk3  40871  dia2dimlem1  41102  dvheveccl  41150  dihord6apre  41294  dihord6b  41298  coprmdvdsb  43017  harval3  43570  monoordxrv  45518  stoweid  46100  smonoord  47401  iccpartgt  47457  goldbachthlem2  47576  lighneallem2  47636  tgoldbach  47847  nn0sumltlt  48380  dignn0flhalflem1  48646