Theorem mpan2d 707

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpand  708  mpan2i  710  ralxfrd  5374  ralxfrd2  5378  sotri3  6136  predtrss  6343  oeordi  8624  coflton  8708  cofon1  8709  cofon2  8710  ttrclss  9748  alephle  10194  axdc3lem4  10558  dedekindle  11501  addlsub  11759  letrp1  12188  ledivp1  12246  peano2uz2  12814  uzind  12818  xrre  13326  xrre2  13327  xrltmin  13339  xrlemin  13341  lemaxle  13352  xralrple  13362  xlemul1a  13445  xrinfmsslem  13465  flge  13972  flflp1  13974  fsequb  14145  seqcl2  14190  monoord  14202  facwordi  14460  facavg  14472  01sqrexlem6  15443  leabs  15495  caubnd  15555  limsupgre  15677  limsupbnd2  15679  lo1bdd2  15720  lo1bddrp  15721  o1lo1  15733  o1rlimmul  15815  lo1mul  15824  isercolllem2  15862  climcndslem1  16047  climcndslem2  16048  ruclem3  16430  ruclem9  16435  ruclem12  16438  dvdsmultr1  16495  ltoddhalfle  16560  divalglem0  16592  dvdsgcdb  16747  dfgcd2  16748  coprmgcdb  16853  coprmdvds2  16858  exprmfct  16909  prmdvdsfz  16910  prmfac1  16925  rpexp  16927  eulerthlem2  16988  pcpremul  17050  pcdvdsb  17076  pcprmpw2  17089  pockthlem  17112  prmreclem3  17125  4sqlem11  17162  vdwnnlem3  17204  meetle  18601  latjlej1  18656  latnlej2  18662  clatleglb  18721  mndodconglem  19785  efgsrel  19978  ablfac1b  20316  pgpfac1lem1  20320  lbsextlem2  21467  psdmul  22517  chfacfscmul0  23206  chfacfpmmul0  23210  lmcls  23650  ufileu  24268  ufilcmp  24381  cnpfcf  24390  tsmsxp  24504  prdsbl  24840  reconnlem2  25177  evth  25310  ivthlem2  25803  ivthlem3  25804  ovollb2lem  25839  ovoliunlem2  25854  ovolicc2lem3  25870  ismbf3d  26005  itg2seq  26093  itg2monolem1  26101  dvcnvrelem1  26367  itgsubst  26399  plypf1  26561  coeaddlem  26598  coemullem  26599  ulmcau  26752  abelth  26798  wilth  27428  ftalem2  27431  ftalem3  27432  muval1  27490  dvdssqf  27495  sqff1o  27539  chtub  27569  bposlem3  27643  lgsne0  27692  gausslemma2dlem1a  27722  gausslemma2dlem2  27724  lgseisenlem1  27732  lgseisenlem2  27733  lgsquadlem1  27737  lgsquadlem2  27738  lgsquadlem3  27739  lgsquad2lem1  27741  lgsquad2lem2  27742  dchrisum0lem1  27873  pntlem3  27966  negbdaylem  28472  mulsproplem5  28536  mulsproplem8  28539  bdayons  28692  z12bdaylem1  28886  upgrewlkle2  30217  pthdlem1  30382  crctcshwlkn0lem3  30431  ex-natded5.8-2  31045  nmoub3i  31405  ubthlem1  31502  ubthlem2  31503  shsel1  31953  nmopub2tALT  32541  nmfnleub2  32558  lnconi  32665  eulerpartlemb  35070  karddom  35929  kardsdom  35930  dfon2lem4  36726  btwncomim  36956  ltnmul  37143  nn0prpwlem  37288  cgsex2gd  38250  ltflcei  38723  poimirlem9  38739  poimirlem18  38748  poimirlem21  38751  poimirlem22  38752  poimirlem24  38754  poimirlem29  38759  heicant  38765  mbfresfi  38776  itg2addnclem2  38782  itg2addnclem3  38783  incsequz  38874  heibor1lem  38935  atlelt  40687  1cvratex  40722  dalem3  40913  linepsubN  41001  pmapsub  41017  2llnma3r  41037  cdlemblem  41042  pmapjoin  41101  atmod1i1  41106  atmod1i2  41108  llnmod1i2  41109  lhpmcvr4N  41275  4atexlemnclw  41319  cdlemd3  41449  cdleme3g  41483  cdleme3h  41484  cdleme7d  41495  cdleme7ga  41497  cdleme21c  41576  cdleme35fnpq  41698  cdleme35f  41703  cdlemf1  41810  cdlemg4  41866  cdlemg6c  41869  cdlemg27a  41941  cdlemg33b0  41950  cdlemg33a  41955  cdlemk3  42082  dia2dimlem1  42313  dvheveccl  42361  dihord6apre  42505  dihord6b  42509  coprmdvdsb  44185  harval3  44731  monoordxrv  46696  stoweid  47278  smonoord  48652  iccpartgt  48714  goldbachthlem2  48836  lighneallem2  48896  tgoldbach  49120  nn0sumltlt  49667  dignn0flhalflem1  49932