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  5413  ralxfrd2  5417  sotri3  6152  predtrss  6344  oeordi  8623  coflton  8707  cofon1  8708  cofon2  8709  xpfiOLD  9356  ttrclss  9757  alephle  10125  axdc3lem4  10490  dedekindle  11422  addlsub  11676  letrp1  12108  ledivp1  12167  peano2uz2  12703  uzind  12707  xrre  13207  xrre2  13208  xrltmin  13220  xrlemin  13222  lemaxle  13233  xralrple  13243  xlemul1a  13326  xrinfmsslem  13346  flge  13841  flflp1  13843  fsequb  14012  seqcl2  14057  monoord  14069  facwordi  14324  facavg  14336  01sqrexlem6  15282  leabs  15334  caubnd  15393  limsupgre  15513  limsupbnd2  15515  lo1bdd2  15556  lo1bddrp  15557  o1lo1  15569  o1rlimmul  15651  lo1mul  15660  isercolllem2  15698  climcndslem1  15881  climcndslem2  15882  ruclem3  16265  ruclem9  16270  ruclem12  16273  dvdsmultr1  16329  ltoddhalfle  16394  divalglem0  16426  dvdsgcdb  16578  dfgcd2  16579  coprmgcdb  16682  coprmdvds2  16687  exprmfct  16737  prmdvdsfz  16738  prmfac1  16753  rpexp  16755  eulerthlem2  16815  pcpremul  16876  pcdvdsb  16902  pcprmpw2  16915  pockthlem  16938  prmreclem3  16951  4sqlem11  16988  vdwnnlem3  17030  meetle  18457  latjlej1  18510  latnlej2  18516  clatleglb  18575  mndodconglem  19573  efgsrel  19766  ablfac1b  20104  pgpfac1lem1  20108  lbsextlem2  21178  psdmul  22187  chfacfscmul0  22879  chfacfpmmul0  22883  lmcls  23325  ufileu  23942  ufilcmp  24055  cnpfcf  24064  tsmsxp  24178  prdsbl  24519  reconnlem2  24862  evth  25004  ivthlem2  25500  ivthlem3  25501  ovollb2lem  25536  ovoliunlem2  25551  ovolicc2lem3  25567  ismbf3d  25702  itg2seq  25791  itg2monolem1  25799  dvcnvrelem1  26070  itgsubst  26104  plypf1  26265  coeaddlem  26302  coemullem  26303  ulmcau  26452  abelth  26499  wilth  27128  ftalem2  27131  ftalem3  27132  muval1  27190  dvdssqf  27195  sqff1o  27239  chtub  27270  bposlem3  27344  lgsne0  27393  gausslemma2dlem1a  27423  gausslemma2dlem2  27425  lgseisenlem1  27433  lgseisenlem2  27434  lgsquadlem1  27438  lgsquadlem2  27439  lgsquadlem3  27440  lgsquad2lem1  27442  lgsquad2lem2  27443  dchrisum0lem1  27574  pntlem3  27667  negsbdaylem  28102  mulsproplem5  28160  mulsproplem8  28163  upgrewlkle2  29638  pthdlem1  29798  crctcshwlkn0lem3  29841  ex-natded5.8-2  30442  nmoub3i  30801  ubthlem1  30898  ubthlem2  30899  shsel1  31349  nmopub2tALT  31937  nmfnleub2  31954  lnconi  32061  eulerpartlemb  34349  dfon2lem4  35767  btwncomim  35994  nn0prpwlem  36304  ltflcei  37594  poimirlem9  37615  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem24  37630  poimirlem29  37635  heicant  37641  mbfresfi  37652  itg2addnclem2  37658  itg2addnclem3  37659  incsequz  37734  heibor1lem  37795  atlelt  39420  1cvratex  39455  dalem3  39646  linepsubN  39734  pmapsub  39750  2llnma3r  39770  cdlemblem  39775  pmapjoin  39834  atmod1i1  39839  atmod1i2  39841  llnmod1i2  39842  lhpmcvr4N  40008  4atexlemnclw  40052  cdlemd3  40182  cdleme3g  40216  cdleme3h  40217  cdleme7d  40228  cdleme7ga  40230  cdleme21c  40309  cdleme35fnpq  40431  cdleme35f  40436  cdlemf1  40543  cdlemg4  40599  cdlemg6c  40602  cdlemg27a  40674  cdlemg33b0  40683  cdlemg33a  40688  cdlemk3  40815  dia2dimlem1  41046  dvheveccl  41094  dihord6apre  41238  dihord6b  41242  coprmdvdsb  42973  harval3  43527  monoordxrv  45431  stoweid  46018  smonoord  47295  iccpartgt  47351  goldbachthlem2  47470  lighneallem2  47530  tgoldbach  47741  nn0sumltlt  48194  dignn0flhalflem1  48464