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

This theorem is referenced by:  mpand  695  mpan2i  697  ralxfrd  5286  ralxfrd2  5290  sotri3  5975  oeordi  8293  xpfi  8920  alephle  9667  axdc3lem4  10032  dedekindle  10961  addlsub  11213  letrp1  11641  ledivp1  11699  peano2uz2  12230  uzind  12234  xrre  12724  xrre2  12725  xrltmin  12737  xrlemin  12739  lemaxle  12750  xralrple  12760  xlemul1a  12843  xrinfmsslem  12863  flge  13345  flflp1  13347  fsequb  13513  seqcl2  13559  monoord  13571  facwordi  13820  facavg  13832  sqrlem6  14776  leabs  14828  caubnd  14887  limsupgre  15007  limsupbnd2  15009  lo1bdd2  15050  lo1bddrp  15051  o1lo1  15063  o1rlimmul  15145  lo1mul  15154  isercolllem2  15194  climcndslem1  15376  climcndslem2  15377  ruclem3  15757  ruclem9  15762  ruclem12  15765  dvdsmultr1  15820  ltoddhalfle  15885  divalglem0  15917  dvdsgcdb  16068  dfgcd2  16069  coprmgcdb  16169  coprmdvds2  16174  exprmfct  16224  prmdvdsfz  16225  prmfac1  16241  rpexp  16242  eulerthlem2  16298  pcpremul  16359  pcdvdsb  16385  pcprmpw2  16398  pockthlem  16421  prmreclem3  16434  4sqlem11  16471  vdwnnlem3  16513  meetle  17860  latjlej1  17913  latnlej2  17919  clatleglb  17978  mndodconglem  18887  efgsrel  19078  ablfac1b  19411  pgpfac1lem1  19415  lbsextlem2  20150  chfacfscmul0  21709  chfacfpmmul0  21713  lmcls  22153  ufileu  22770  ufilcmp  22883  cnpfcf  22892  tsmsxp  23006  prdsbl  23343  reconnlem2  23678  evth  23810  ivthlem2  24303  ivthlem3  24304  ovollb2lem  24339  ovoliunlem2  24354  ovolicc2lem3  24370  ismbf3d  24505  itg2seq  24594  itg2monolem1  24602  dvcnvrelem1  24868  itgsubst  24900  plypf1  25060  coeaddlem  25097  coemullem  25098  ulmcau  25241  abelth  25287  wilth  25907  ftalem2  25910  ftalem3  25911  muval1  25969  dvdssqf  25974  sqff1o  26018  chtub  26047  bposlem3  26121  lgsne0  26170  gausslemma2dlem1a  26200  gausslemma2dlem2  26202  lgseisenlem1  26210  lgseisenlem2  26211  lgsquadlem1  26215  lgsquadlem2  26216  lgsquadlem3  26217  lgsquad2lem1  26219  lgsquad2lem2  26220  dchrisum0lem1  26351  pntlem3  26444  upgrewlkle2  27648  pthdlem1  27807  crctcshwlkn0lem3  27850  ex-natded5.8-2  28451  nmoub3i  28808  ubthlem1  28905  ubthlem2  28906  shsel1  29356  nmopub2tALT  29944  nmfnleub2  29961  lnconi  30068  eulerpartlemb  32001  dfon2lem4  33432  btwncomim  34001  nn0prpwlem  34197  ltflcei  35451  poimirlem9  35472  poimirlem18  35481  poimirlem21  35484  poimirlem22  35485  poimirlem24  35487  poimirlem29  35492  heicant  35498  mbfresfi  35509  itg2addnclem2  35515  itg2addnclem3  35516  incsequz  35592  heibor1lem  35653  atlelt  37138  1cvratex  37173  dalem3  37364  linepsubN  37452  pmapsub  37468  2llnma3r  37488  cdlemblem  37493  pmapjoin  37552  atmod1i1  37557  atmod1i2  37559  llnmod1i2  37560  lhpmcvr4N  37726  4atexlemnclw  37770  cdlemd3  37900  cdleme3g  37934  cdleme3h  37935  cdleme7d  37946  cdleme7ga  37948  cdleme21c  38027  cdleme35fnpq  38149  cdleme35f  38154  cdlemf1  38261  cdlemg4  38317  cdlemg6c  38320  cdlemg27a  38392  cdlemg33b0  38401  cdlemg33a  38406  cdlemk3  38533  dia2dimlem1  38764  dvheveccl  38812  dihord6apre  38956  dihord6b  38960  coprmdvdsb  40451  harval3  40769  monoordxrv  42638  stoweid  43222  smonoord  44439  iccpartgt  44495  goldbachthlem2  44614  lighneallem2  44674  tgoldbach  44885  nn0sumltlt  45302  dignn0flhalflem1  45577