Theorem mpan2d 693

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mpand  694  mpan2i  696  ralxfrd  5406  ralxfrd2  5410  sotri3  6129  predtrss  6321  oeordi  8584  coflton  8667  cofon1  8668  cofon2  8669  xpfiOLD  9315  ttrclss  9712  alephle  10080  axdc3lem4  10445  dedekindle  11375  addlsub  11627  letrp1  12055  ledivp1  12113  peano2uz2  12647  uzind  12651  xrre  13145  xrre2  13146  xrltmin  13158  xrlemin  13160  lemaxle  13171  xralrple  13181  xlemul1a  13264  xrinfmsslem  13284  flge  13767  flflp1  13769  fsequb  13937  seqcl2  13983  monoord  13995  facwordi  14246  facavg  14258  01sqrexlem6  15191  leabs  15243  caubnd  15302  limsupgre  15422  limsupbnd2  15424  lo1bdd2  15465  lo1bddrp  15466  o1lo1  15478  o1rlimmul  15560  lo1mul  15569  isercolllem2  15609  climcndslem1  15792  climcndslem2  15793  ruclem3  16173  ruclem9  16178  ruclem12  16181  dvdsmultr1  16236  ltoddhalfle  16301  divalglem0  16333  dvdsgcdb  16484  dfgcd2  16485  coprmgcdb  16583  coprmdvds2  16588  exprmfct  16638  prmdvdsfz  16639  prmfac1  16655  rpexp  16656  eulerthlem2  16712  pcpremul  16773  pcdvdsb  16799  pcprmpw2  16812  pockthlem  16835  prmreclem3  16848  4sqlem11  16885  vdwnnlem3  16927  meetle  18350  latjlej1  18403  latnlej2  18409  clatleglb  18468  mndodconglem  19404  efgsrel  19597  ablfac1b  19935  pgpfac1lem1  19939  lbsextlem2  20765  chfacfscmul0  22352  chfacfpmmul0  22356  lmcls  22798  ufileu  23415  ufilcmp  23528  cnpfcf  23537  tsmsxp  23651  prdsbl  23992  reconnlem2  24335  evth  24467  ivthlem2  24961  ivthlem3  24962  ovollb2lem  24997  ovoliunlem2  25012  ovolicc2lem3  25028  ismbf3d  25163  itg2seq  25252  itg2monolem1  25260  dvcnvrelem1  25526  itgsubst  25558  plypf1  25718  coeaddlem  25755  coemullem  25756  ulmcau  25899  abelth  25945  wilth  26565  ftalem2  26568  ftalem3  26569  muval1  26627  dvdssqf  26632  sqff1o  26676  chtub  26705  bposlem3  26779  lgsne0  26828  gausslemma2dlem1a  26858  gausslemma2dlem2  26860  lgseisenlem1  26868  lgseisenlem2  26869  lgsquadlem1  26873  lgsquadlem2  26874  lgsquadlem3  26875  lgsquad2lem1  26877  lgsquad2lem2  26878  dchrisum0lem1  27009  pntlem3  27102  negsbdaylem  27520  mulsproplem5  27566  mulsproplem8  27569  upgrewlkle2  28853  pthdlem1  29013  crctcshwlkn0lem3  29056  ex-natded5.8-2  29657  nmoub3i  30014  ubthlem1  30111  ubthlem2  30112  shsel1  30562  nmopub2tALT  31150  nmfnleub2  31167  lnconi  31274  eulerpartlemb  33356  dfon2lem4  34747  btwncomim  34974  nn0prpwlem  35196  ltflcei  36465  poimirlem9  36486  poimirlem18  36495  poimirlem21  36498  poimirlem22  36499  poimirlem24  36501  poimirlem29  36506  heicant  36512  mbfresfi  36523  itg2addnclem2  36529  itg2addnclem3  36530  incsequz  36605  heibor1lem  36666  atlelt  38298  1cvratex  38333  dalem3  38524  linepsubN  38612  pmapsub  38628  2llnma3r  38648  cdlemblem  38653  pmapjoin  38712  atmod1i1  38717  atmod1i2  38719  llnmod1i2  38720  lhpmcvr4N  38886  4atexlemnclw  38930  cdlemd3  39060  cdleme3g  39094  cdleme3h  39095  cdleme7d  39106  cdleme7ga  39108  cdleme21c  39187  cdleme35fnpq  39309  cdleme35f  39314  cdlemf1  39421  cdlemg4  39477  cdlemg6c  39480  cdlemg27a  39552  cdlemg33b0  39561  cdlemg33a  39566  cdlemk3  39693  dia2dimlem1  39924  dvheveccl  39972  dihord6apre  40116  dihord6b  40120  coprmdvdsb  41710  harval3  42275  monoordxrv  44179  stoweid  44766  smonoord  46026  iccpartgt  46082  goldbachthlem2  46201  lighneallem2  46261  tgoldbach  46472  nn0sumltlt  46980  dignn0flhalflem1  47255