Theorem mpan2d 706

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 420	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
4	1, 3	mpid 45	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpand  707  mpan2i  709  ralxfrd  5370  ralxfrd2  5374  sotri3  6121  predtrss  6313  oeordi  8561  coflton  8645  cofon1  8646  cofon2  8647  ttrclss  9677  alephle  10060  axdc3lem4  10425  dedekindle  11362  addlsub  11618  letrp1  12050  ledivp1  12108  peano2uz2  12675  uzind  12679  xrre  13186  xrre2  13187  xrltmin  13199  xrlemin  13201  lemaxle  13212  xralrple  13222  xlemul1a  13305  xrinfmsslem  13325  flge  13829  flflp1  13831  fsequb  14002  seqcl2  14047  monoord  14059  facwordi  14316  facavg  14328  01sqrexlem6  15288  leabs  15340  caubnd  15400  limsupgre  15522  limsupbnd2  15524  lo1bdd2  15565  lo1bddrp  15566  o1lo1  15578  o1rlimmul  15660  lo1mul  15669  isercolllem2  15707  climcndslem1  15893  climcndslem2  15894  ruclem3  16279  ruclem9  16284  ruclem12  16287  dvdsmultr1  16344  ltoddhalfle  16409  divalglem0  16441  dvdsgcdb  16593  dfgcd2  16594  coprmgcdb  16697  coprmdvds2  16702  exprmfct  16753  prmdvdsfz  16754  prmfac1  16769  rpexp  16771  eulerthlem2  16831  pcpremul  16893  pcdvdsb  16919  pcprmpw2  16932  pockthlem  16955  prmreclem3  16968  4sqlem11  17005  vdwnnlem3  17047  meetle  18444  latjlej1  18499  latnlej2  18505  clatleglb  18564  mndodconglem  19602  efgsrel  19795  ablfac1b  20133  pgpfac1lem1  20137  lbsextlem2  21252  psdmul  22289  chfacfscmul0  22976  chfacfpmmul0  22980  lmcls  23420  ufileu  24037  ufilcmp  24150  cnpfcf  24159  tsmsxp  24273  prdsbl  24609  reconnlem2  24946  evth  25079  ivthlem2  25572  ivthlem3  25573  ovollb2lem  25608  ovoliunlem2  25623  ovolicc2lem3  25639  ismbf3d  25774  itg2seq  25862  itg2monolem1  25870  dvcnvrelem1  26137  itgsubst  26169  plypf1  26330  coeaddlem  26367  coemullem  26368  ulmcau  26516  abelth  26562  wilth  27193  ftalem2  27196  ftalem3  27197  muval1  27255  dvdssqf  27260  sqff1o  27304  chtub  27334  bposlem3  27408  lgsne0  27457  gausslemma2dlem1a  27487  gausslemma2dlem2  27489  lgseisenlem1  27497  lgseisenlem2  27498  lgsquadlem1  27502  lgsquadlem2  27503  lgsquadlem3  27504  lgsquad2lem1  27506  lgsquad2lem2  27507  dchrisum0lem1  27638  pntlem3  27731  negbdaylem  28207  mulsproplem5  28271  mulsproplem8  28274  bdayons  28427  z12bdaylem1  28621  upgrewlkle2  29865  pthdlem1  30024  crctcshwlkn0lem3  30070  ex-natded5.8-2  30674  nmoub3i  31034  ubthlem1  31131  ubthlem2  31132  shsel1  31582  nmopub2tALT  32170  nmfnleub2  32187  lnconi  32294  eulerpartlemb  34675  r1elcl  35406  dfon2lem4  36147  btwncomim  36376  nn0prpwlem  36695  cgsex2gd  37641  ltflcei  38119  poimirlem9  38140  poimirlem18  38149  poimirlem21  38152  poimirlem22  38153  poimirlem24  38155  poimirlem29  38160  heicant  38166  mbfresfi  38177  itg2addnclem2  38183  itg2addnclem3  38184  incsequz  38259  heibor1lem  38320  atlelt  40074  1cvratex  40109  dalem3  40300  linepsubN  40388  pmapsub  40404  2llnma3r  40424  cdlemblem  40429  pmapjoin  40488  atmod1i1  40493  atmod1i2  40495  llnmod1i2  40496  lhpmcvr4N  40662  4atexlemnclw  40706  cdlemd3  40836  cdleme3g  40870  cdleme3h  40871  cdleme7d  40882  cdleme7ga  40884  cdleme21c  40963  cdleme35fnpq  41085  cdleme35f  41090  cdlemf1  41197  cdlemg4  41253  cdlemg6c  41256  cdlemg27a  41328  cdlemg33b0  41337  cdlemg33a  41342  cdlemk3  41469  dia2dimlem1  41700  dvheveccl  41748  dihord6apre  41892  dihord6b  41896  coprmdvdsb  43574  harval3  44126  monoordxrv  46053  stoweid  46635  smonoord  47969  iccpartgt  48031  goldbachthlem2  48153  lighneallem2  48213  tgoldbach  48437  nn0sumltlt  48981  dignn0flhalflem1  49246