Theorem mpan2d 704

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  mpand  705  mpan2i  707  ralxfrd  5364  ralxfrd2  5368  sotri3  6114  predtrss  6305  oeordi  8552  coflton  8636  cofon1  8637  cofon2  8638  ttrclss  9672  alephle  10041  axdc3lem4  10407  dedekindle  11344  addlsub  11600  letrp1  12032  ledivp1  12091  peano2uz2  12658  uzind  12662  xrre  13169  xrre2  13170  xrltmin  13182  xrlemin  13184  lemaxle  13195  xralrple  13205  xlemul1a  13288  xrinfmsslem  13308  flge  13812  flflp1  13814  fsequb  13985  seqcl2  14030  monoord  14042  facwordi  14299  facavg  14311  01sqrexlem6  15257  leabs  15309  caubnd  15369  limsupgre  15491  limsupbnd2  15493  lo1bdd2  15534  lo1bddrp  15535  o1lo1  15547  o1rlimmul  15629  lo1mul  15638  isercolllem2  15676  climcndslem1  15862  climcndslem2  15863  ruclem3  16248  ruclem9  16253  ruclem12  16256  dvdsmultr1  16313  ltoddhalfle  16378  divalglem0  16410  dvdsgcdb  16562  dfgcd2  16563  coprmgcdb  16666  coprmdvds2  16671  exprmfct  16722  prmdvdsfz  16723  prmfac1  16738  rpexp  16740  eulerthlem2  16800  pcpremul  16862  pcdvdsb  16888  pcprmpw2  16901  pockthlem  16924  prmreclem3  16937  4sqlem11  16974  vdwnnlem3  17016  meetle  18413  latjlej1  18468  latnlej2  18474  clatleglb  18533  mndodconglem  19564  efgsrel  19757  ablfac1b  20095  pgpfac1lem1  20099  lbsextlem2  21209  psdmul  22211  chfacfscmul0  22898  chfacfpmmul0  22902  lmcls  23342  ufileu  23959  ufilcmp  24072  cnpfcf  24081  tsmsxp  24195  prdsbl  24531  reconnlem2  24868  evth  25001  ivthlem2  25494  ivthlem3  25495  ovollb2lem  25530  ovoliunlem2  25545  ovolicc2lem3  25561  ismbf3d  25696  itg2seq  25784  itg2monolem1  25792  dvcnvrelem1  26059  itgsubst  26091  plypf1  26252  coeaddlem  26289  coemullem  26290  ulmcau  26435  abelth  26481  wilth  27112  ftalem2  27115  ftalem3  27116  muval1  27174  dvdssqf  27179  sqff1o  27223  chtub  27253  bposlem3  27327  lgsne0  27376  gausslemma2dlem1a  27406  gausslemma2dlem2  27408  lgseisenlem1  27416  lgseisenlem2  27417  lgsquadlem1  27421  lgsquadlem2  27422  lgsquadlem3  27423  lgsquad2lem1  27425  lgsquad2lem2  27426  dchrisum0lem1  27557  pntlem3  27650  negbdaylem  28126  mulsproplem5  28190  mulsproplem8  28193  bdayons  28346  z12bdaylem1  28540  upgrewlkle2  29753  pthdlem1  29912  crctcshwlkn0lem3  29958  ex-natded5.8-2  30562  nmoub3i  30922  ubthlem1  31019  ubthlem2  31020  shsel1  31470  nmopub2tALT  32058  nmfnleub2  32075  lnconi  32182  eulerpartlemb  34626  r1elcl  35358  dfon2lem4  36098  btwncomim  36327  nn0prpwlem  36646  cgsex2gd  37593  ltflcei  38071  poimirlem9  38092  poimirlem18  38101  poimirlem21  38104  poimirlem22  38105  poimirlem24  38107  poimirlem29  38112  heicant  38118  mbfresfi  38129  itg2addnclem2  38135  itg2addnclem3  38136  incsequz  38211  heibor1lem  38272  atlelt  40026  1cvratex  40061  dalem3  40252  linepsubN  40340  pmapsub  40356  2llnma3r  40376  cdlemblem  40381  pmapjoin  40440  atmod1i1  40445  atmod1i2  40447  llnmod1i2  40448  lhpmcvr4N  40614  4atexlemnclw  40658  cdlemd3  40788  cdleme3g  40822  cdleme3h  40823  cdleme7d  40834  cdleme7ga  40836  cdleme21c  40915  cdleme35fnpq  41037  cdleme35f  41042  cdlemf1  41149  cdlemg4  41205  cdlemg6c  41208  cdlemg27a  41280  cdlemg33b0  41289  cdlemg33a  41294  cdlemk3  41421  dia2dimlem1  41652  dvheveccl  41700  dihord6apre  41844  dihord6b  41848  coprmdvdsb  43526  harval3  44078  monoordxrv  46019  stoweid  46601  smonoord  47935  iccpartgt  47997  goldbachthlem2  48119  lighneallem2  48179  tgoldbach  48403  nn0sumltlt  48936  dignn0flhalflem1  49201