Theorem mpan2d 691

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  mpand  692  mpan2i  694  ralxfrd  5332  ralxfrd2  5336  sotri3  6040  predtrss  6229  oeordi  8427  xpfi  9094  ttrclss  9487  alephle  9853  axdc3lem4  10218  dedekindle  11148  addlsub  11400  letrp1  11828  ledivp1  11886  peano2uz2  12417  uzind  12421  xrre  12912  xrre2  12913  xrltmin  12925  xrlemin  12927  lemaxle  12938  xralrple  12948  xlemul1a  13031  xrinfmsslem  13051  flge  13534  flflp1  13536  fsequb  13704  seqcl2  13750  monoord  13762  facwordi  14012  facavg  14024  sqrlem6  14968  leabs  15020  caubnd  15079  limsupgre  15199  limsupbnd2  15201  lo1bdd2  15242  lo1bddrp  15243  o1lo1  15255  o1rlimmul  15337  lo1mul  15346  isercolllem2  15386  climcndslem1  15570  climcndslem2  15571  ruclem3  15951  ruclem9  15956  ruclem12  15959  dvdsmultr1  16014  ltoddhalfle  16079  divalglem0  16111  dvdsgcdb  16262  dfgcd2  16263  coprmgcdb  16363  coprmdvds2  16368  exprmfct  16418  prmdvdsfz  16419  prmfac1  16435  rpexp  16436  eulerthlem2  16492  pcpremul  16553  pcdvdsb  16579  pcprmpw2  16592  pockthlem  16615  prmreclem3  16628  4sqlem11  16665  vdwnnlem3  16707  meetle  18127  latjlej1  18180  latnlej2  18186  clatleglb  18245  mndodconglem  19158  efgsrel  19349  ablfac1b  19682  pgpfac1lem1  19686  lbsextlem2  20430  chfacfscmul0  22016  chfacfpmmul0  22020  lmcls  22462  ufileu  23079  ufilcmp  23192  cnpfcf  23201  tsmsxp  23315  prdsbl  23656  reconnlem2  23999  evth  24131  ivthlem2  24625  ivthlem3  24626  ovollb2lem  24661  ovoliunlem2  24676  ovolicc2lem3  24692  ismbf3d  24827  itg2seq  24916  itg2monolem1  24924  dvcnvrelem1  25190  itgsubst  25222  plypf1  25382  coeaddlem  25419  coemullem  25420  ulmcau  25563  abelth  25609  wilth  26229  ftalem2  26232  ftalem3  26233  muval1  26291  dvdssqf  26296  sqff1o  26340  chtub  26369  bposlem3  26443  lgsne0  26492  gausslemma2dlem1a  26522  gausslemma2dlem2  26524  lgseisenlem1  26532  lgseisenlem2  26533  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  lgsquad2lem1  26541  lgsquad2lem2  26542  dchrisum0lem1  26673  pntlem3  26766  upgrewlkle2  27982  pthdlem1  28143  crctcshwlkn0lem3  28186  ex-natded5.8-2  28787  nmoub3i  29144  ubthlem1  29241  ubthlem2  29242  shsel1  29692  nmopub2tALT  30280  nmfnleub2  30297  lnconi  30404  eulerpartlemb  32344  dfon2lem4  33771  btwncomim  34324  nn0prpwlem  34520  ltflcei  35774  poimirlem9  35795  poimirlem18  35804  poimirlem21  35807  poimirlem22  35808  poimirlem24  35810  poimirlem29  35815  heicant  35821  mbfresfi  35832  itg2addnclem2  35838  itg2addnclem3  35839  incsequz  35915  heibor1lem  35976  atlelt  37459  1cvratex  37494  dalem3  37685  linepsubN  37773  pmapsub  37789  2llnma3r  37809  cdlemblem  37814  pmapjoin  37873  atmod1i1  37878  atmod1i2  37880  llnmod1i2  37881  lhpmcvr4N  38047  4atexlemnclw  38091  cdlemd3  38221  cdleme3g  38255  cdleme3h  38256  cdleme7d  38267  cdleme7ga  38269  cdleme21c  38348  cdleme35fnpq  38470  cdleme35f  38475  cdlemf1  38582  cdlemg4  38638  cdlemg6c  38641  cdlemg27a  38713  cdlemg33b0  38722  cdlemg33a  38727  cdlemk3  38854  dia2dimlem1  39085  dvheveccl  39133  dihord6apre  39277  dihord6b  39281  coprmdvdsb  40814  harval3  41152  monoordxrv  43029  stoweid  43611  smonoord  44834  iccpartgt  44890  goldbachthlem2  45009  lighneallem2  45069  tgoldbach  45280  nn0sumltlt  45697  dignn0flhalflem1  45972