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  5408  ralxfrd2  5412  sotri3  6150  predtrss  6343  oeordi  8625  coflton  8709  cofon1  8710  cofon2  8711  xpfiOLD  9359  ttrclss  9760  alephle  10128  axdc3lem4  10493  dedekindle  11425  addlsub  11679  letrp1  12111  ledivp1  12170  peano2uz2  12706  uzind  12710  xrre  13211  xrre2  13212  xrltmin  13224  xrlemin  13226  lemaxle  13237  xralrple  13247  xlemul1a  13330  xrinfmsslem  13350  flge  13845  flflp1  13847  fsequb  14016  seqcl2  14061  monoord  14073  facwordi  14328  facavg  14340  01sqrexlem6  15286  leabs  15338  caubnd  15397  limsupgre  15517  limsupbnd2  15519  lo1bdd2  15560  lo1bddrp  15561  o1lo1  15573  o1rlimmul  15655  lo1mul  15664  isercolllem2  15702  climcndslem1  15885  climcndslem2  15886  ruclem3  16269  ruclem9  16274  ruclem12  16277  dvdsmultr1  16333  ltoddhalfle  16398  divalglem0  16430  dvdsgcdb  16582  dfgcd2  16583  coprmgcdb  16686  coprmdvds2  16691  exprmfct  16741  prmdvdsfz  16742  prmfac1  16757  rpexp  16759  eulerthlem2  16819  pcpremul  16881  pcdvdsb  16907  pcprmpw2  16920  pockthlem  16943  prmreclem3  16956  4sqlem11  16993  vdwnnlem3  17035  meetle  18445  latjlej1  18498  latnlej2  18504  clatleglb  18563  mndodconglem  19559  efgsrel  19752  ablfac1b  20090  pgpfac1lem1  20094  lbsextlem2  21161  psdmul  22170  chfacfscmul0  22864  chfacfpmmul0  22868  lmcls  23310  ufileu  23927  ufilcmp  24040  cnpfcf  24049  tsmsxp  24163  prdsbl  24504  reconnlem2  24849  evth  24991  ivthlem2  25487  ivthlem3  25488  ovollb2lem  25523  ovoliunlem2  25538  ovolicc2lem3  25554  ismbf3d  25689  itg2seq  25777  itg2monolem1  25785  dvcnvrelem1  26056  itgsubst  26090  plypf1  26251  coeaddlem  26288  coemullem  26289  ulmcau  26438  abelth  26485  wilth  27114  ftalem2  27117  ftalem3  27118  muval1  27176  dvdssqf  27181  sqff1o  27225  chtub  27256  bposlem3  27330  lgsne0  27379  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  lgseisenlem1  27419  lgseisenlem2  27420  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  lgsquad2lem1  27428  lgsquad2lem2  27429  dchrisum0lem1  27560  pntlem3  27653  negsbdaylem  28088  mulsproplem5  28146  mulsproplem8  28149  upgrewlkle2  29624  pthdlem1  29786  crctcshwlkn0lem3  29832  ex-natded5.8-2  30433  nmoub3i  30792  ubthlem1  30889  ubthlem2  30890  shsel1  31340  nmopub2tALT  31928  nmfnleub2  31945  lnconi  32052  eulerpartlemb  34370  dfon2lem4  35787  btwncomim  36014  nn0prpwlem  36323  ltflcei  37615  poimirlem9  37636  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem24  37651  poimirlem29  37656  heicant  37662  mbfresfi  37673  itg2addnclem2  37679  itg2addnclem3  37680  incsequz  37755  heibor1lem  37816  atlelt  39440  1cvratex  39475  dalem3  39666  linepsubN  39754  pmapsub  39770  2llnma3r  39790  cdlemblem  39795  pmapjoin  39854  atmod1i1  39859  atmod1i2  39861  llnmod1i2  39862  lhpmcvr4N  40028  4atexlemnclw  40072  cdlemd3  40202  cdleme3g  40236  cdleme3h  40237  cdleme7d  40248  cdleme7ga  40250  cdleme21c  40329  cdleme35fnpq  40451  cdleme35f  40456  cdlemf1  40563  cdlemg4  40619  cdlemg6c  40622  cdlemg27a  40694  cdlemg33b0  40703  cdlemg33a  40708  cdlemk3  40835  dia2dimlem1  41066  dvheveccl  41114  dihord6apre  41258  dihord6b  41262  coprmdvdsb  42997  harval3  43551  monoordxrv  45492  stoweid  46078  smonoord  47358  iccpartgt  47414  goldbachthlem2  47533  lighneallem2  47593  tgoldbach  47804  nn0sumltlt  48266  dignn0flhalflem1  48536