Theorem mpan2d 693

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  694  mpan2i  696  ralxfrd  5426  ralxfrd2  5430  sotri3  6162  predtrss  6354  oeordi  8643  coflton  8727  cofon1  8728  cofon2  8729  xpfiOLD  9387  ttrclss  9789  alephle  10157  axdc3lem4  10522  dedekindle  11454  addlsub  11706  letrp1  12138  ledivp1  12197  peano2uz2  12731  uzind  12735  xrre  13231  xrre2  13232  xrltmin  13244  xrlemin  13246  lemaxle  13257  xralrple  13267  xlemul1a  13350  xrinfmsslem  13370  flge  13856  flflp1  13858  fsequb  14026  seqcl2  14071  monoord  14083  facwordi  14338  facavg  14350  01sqrexlem6  15296  leabs  15348  caubnd  15407  limsupgre  15527  limsupbnd2  15529  lo1bdd2  15570  lo1bddrp  15571  o1lo1  15583  o1rlimmul  15665  lo1mul  15674  isercolllem2  15714  climcndslem1  15897  climcndslem2  15898  ruclem3  16281  ruclem9  16286  ruclem12  16289  dvdsmultr1  16344  ltoddhalfle  16409  divalglem0  16441  dvdsgcdb  16592  dfgcd2  16593  coprmgcdb  16696  coprmdvds2  16701  exprmfct  16751  prmdvdsfz  16752  prmfac1  16767  rpexp  16769  eulerthlem2  16829  pcpremul  16890  pcdvdsb  16916  pcprmpw2  16929  pockthlem  16952  prmreclem3  16965  4sqlem11  17002  vdwnnlem3  17044  meetle  18470  latjlej1  18523  latnlej2  18529  clatleglb  18588  mndodconglem  19583  efgsrel  19776  ablfac1b  20114  pgpfac1lem1  20118  lbsextlem2  21184  psdmul  22193  chfacfscmul0  22885  chfacfpmmul0  22889  lmcls  23331  ufileu  23948  ufilcmp  24061  cnpfcf  24070  tsmsxp  24184  prdsbl  24525  reconnlem2  24868  evth  25010  ivthlem2  25506  ivthlem3  25507  ovollb2lem  25542  ovoliunlem2  25557  ovolicc2lem3  25573  ismbf3d  25708  itg2seq  25797  itg2monolem1  25805  dvcnvrelem1  26076  itgsubst  26110  plypf1  26271  coeaddlem  26308  coemullem  26309  ulmcau  26456  abelth  26503  wilth  27132  ftalem2  27135  ftalem3  27136  muval1  27194  dvdssqf  27199  sqff1o  27243  chtub  27274  bposlem3  27348  lgsne0  27397  gausslemma2dlem1a  27427  gausslemma2dlem2  27429  lgseisenlem1  27437  lgseisenlem2  27438  lgsquadlem1  27442  lgsquadlem2  27443  lgsquadlem3  27444  lgsquad2lem1  27446  lgsquad2lem2  27447  dchrisum0lem1  27578  pntlem3  27671  negsbdaylem  28106  mulsproplem5  28164  mulsproplem8  28167  upgrewlkle2  29642  pthdlem1  29802  crctcshwlkn0lem3  29845  ex-natded5.8-2  30446  nmoub3i  30805  ubthlem1  30902  ubthlem2  30903  shsel1  31353  nmopub2tALT  31941  nmfnleub2  31958  lnconi  32065  eulerpartlemb  34333  dfon2lem4  35750  btwncomim  35977  nn0prpwlem  36288  ltflcei  37568  poimirlem9  37589  poimirlem18  37598  poimirlem21  37601  poimirlem22  37602  poimirlem24  37604  poimirlem29  37609  heicant  37615  mbfresfi  37626  itg2addnclem2  37632  itg2addnclem3  37633  incsequz  37708  heibor1lem  37769  atlelt  39395  1cvratex  39430  dalem3  39621  linepsubN  39709  pmapsub  39725  2llnma3r  39745  cdlemblem  39750  pmapjoin  39809  atmod1i1  39814  atmod1i2  39816  llnmod1i2  39817  lhpmcvr4N  39983  4atexlemnclw  40027  cdlemd3  40157  cdleme3g  40191  cdleme3h  40192  cdleme7d  40203  cdleme7ga  40205  cdleme21c  40284  cdleme35fnpq  40406  cdleme35f  40411  cdlemf1  40518  cdlemg4  40574  cdlemg6c  40577  cdlemg27a  40649  cdlemg33b0  40658  cdlemg33a  40663  cdlemk3  40790  dia2dimlem1  41021  dvheveccl  41069  dihord6apre  41213  dihord6b  41217  coprmdvdsb  42942  harval3  43500  monoordxrv  45397  stoweid  45984  smonoord  47245  iccpartgt  47301  goldbachthlem2  47420  lighneallem2  47480  tgoldbach  47691  nn0sumltlt  48075  dignn0flhalflem1  48349