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  5363  ralxfrd2  5367  sotri3  6103  predtrss  6295  oeordi  8551  coflton  8635  cofon1  8636  cofon2  8637  xpfiOLD  9270  ttrclss  9673  alephle  10041  axdc3lem4  10406  dedekindle  11338  addlsub  11594  letrp1  12026  ledivp1  12085  peano2uz2  12622  uzind  12626  xrre  13129  xrre2  13130  xrltmin  13142  xrlemin  13144  lemaxle  13155  xralrple  13165  xlemul1a  13248  xrinfmsslem  13268  flge  13767  flflp1  13769  fsequb  13940  seqcl2  13985  monoord  13997  facwordi  14254  facavg  14266  01sqrexlem6  15213  leabs  15265  caubnd  15325  limsupgre  15447  limsupbnd2  15449  lo1bdd2  15490  lo1bddrp  15491  o1lo1  15503  o1rlimmul  15585  lo1mul  15594  isercolllem2  15632  climcndslem1  15815  climcndslem2  15816  ruclem3  16201  ruclem9  16206  ruclem12  16209  dvdsmultr1  16266  ltoddhalfle  16331  divalglem0  16363  dvdsgcdb  16515  dfgcd2  16516  coprmgcdb  16619  coprmdvds2  16624  exprmfct  16674  prmdvdsfz  16675  prmfac1  16690  rpexp  16692  eulerthlem2  16752  pcpremul  16814  pcdvdsb  16840  pcprmpw2  16853  pockthlem  16876  prmreclem3  16889  4sqlem11  16926  vdwnnlem3  16968  meetle  18359  latjlej1  18412  latnlej2  18418  clatleglb  18477  mndodconglem  19471  efgsrel  19664  ablfac1b  20002  pgpfac1lem1  20006  lbsextlem2  21069  psdmul  22053  chfacfscmul0  22745  chfacfpmmul0  22749  lmcls  23189  ufileu  23806  ufilcmp  23919  cnpfcf  23928  tsmsxp  24042  prdsbl  24379  reconnlem2  24716  evth  24858  ivthlem2  25353  ivthlem3  25354  ovollb2lem  25389  ovoliunlem2  25404  ovolicc2lem3  25420  ismbf3d  25555  itg2seq  25643  itg2monolem1  25651  dvcnvrelem1  25922  itgsubst  25956  plypf1  26117  coeaddlem  26154  coemullem  26155  ulmcau  26304  abelth  26351  wilth  26981  ftalem2  26984  ftalem3  26985  muval1  27043  dvdssqf  27048  sqff1o  27092  chtub  27123  bposlem3  27197  lgsne0  27246  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  lgseisenlem1  27286  lgseisenlem2  27287  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  lgsquad2lem1  27295  lgsquad2lem2  27296  dchrisum0lem1  27427  pntlem3  27520  negsbdaylem  27962  mulsproplem5  28023  mulsproplem8  28026  bdayon  28173  upgrewlkle2  29534  pthdlem1  29696  crctcshwlkn0lem3  29742  ex-natded5.8-2  30343  nmoub3i  30702  ubthlem1  30799  ubthlem2  30800  shsel1  31250  nmopub2tALT  31838  nmfnleub2  31855  lnconi  31962  eulerpartlemb  34359  dfon2lem4  35774  btwncomim  36001  nn0prpwlem  36310  ltflcei  37602  poimirlem9  37623  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem24  37638  poimirlem29  37643  heicant  37649  mbfresfi  37660  itg2addnclem2  37666  itg2addnclem3  37667  incsequz  37742  heibor1lem  37803  atlelt  39432  1cvratex  39467  dalem3  39658  linepsubN  39746  pmapsub  39762  2llnma3r  39782  cdlemblem  39787  pmapjoin  39846  atmod1i1  39851  atmod1i2  39853  llnmod1i2  39854  lhpmcvr4N  40020  4atexlemnclw  40064  cdlemd3  40194  cdleme3g  40228  cdleme3h  40229  cdleme7d  40240  cdleme7ga  40242  cdleme21c  40321  cdleme35fnpq  40443  cdleme35f  40448  cdlemf1  40555  cdlemg4  40611  cdlemg6c  40614  cdlemg27a  40686  cdlemg33b0  40695  cdlemg33a  40700  cdlemk3  40827  dia2dimlem1  41058  dvheveccl  41106  dihord6apre  41250  dihord6b  41254  coprmdvdsb  42974  harval3  43527  monoordxrv  45477  stoweid  46061  smonoord  47372  iccpartgt  47428  goldbachthlem2  47547  lighneallem2  47607  tgoldbach  47818  nn0sumltlt  48338  dignn0flhalflem1  48604