Theorem mpan2d 706

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpand  707  mpan2i  709  ralxfrd  4805  ralxfrdOLD  4806  ralxfrd2  4810  sotri3  5445  oeordi  7554  xpfi  8116  alephle  8794  axdc3lem4  9158  dedekindle  10080  addlsub  10326  letrp1  10744  ledivp1  10804  peano2uz2  11341  uzind  11345  xrre  11874  xrre2  11875  xrltmin  11887  xrlemin  11889  lemaxle  11900  xralrple  11910  xlemul1a  11990  xrinfmsslem  12010  flge  12468  flflp1  12470  fsequb  12636  seqcl2  12681  monoord  12693  facwordi  12938  facavg  12950  sqrlem6  13836  leabs  13887  caubnd  13946  limsupgre  14060  limsupbnd2  14062  lo1bdd2  14103  lo1bddrp  14104  o1lo1  14116  o1rlimmul  14197  lo1mul  14206  isercolllem2  14244  climcndslem1  14420  climcndslem2  14421  ruclem3  14801  ruclem9  14806  ruclem12  14809  dvdsmultr1  14857  ltoddhalfle  14923  divalglem0  14954  dvdsgcdb  15100  dfgcd2  15101  coprmgcdb  15200  coprmdvds2  15206  exprmfct  15254  prmdvdsfz  15255  prmfac1  15269  rpexp  15270  eulerthlem2  15325  pcpremul  15386  pcdvdsb  15411  pcprmpw2  15424  pockthlem  15447  prmreclem3  15460  4sqlem11  15497  vdwnnlem3  15539  meetle  16851  latjlej1  16888  latnlej2  16894  clatleglb  16949  mndodconglem  17783  efgsrel  17970  ablfac1b  18292  pgpfac1lem1  18296  lbsextlem2  18980  chfacfscmul0  20482  chfacfpmmul0  20486  lmcls  20916  ufileu  21533  ufilcmp  21646  cnpfcf  21655  tsmsxp  21768  prdsbl  22106  reconnlem2  22438  evth  22566  ivthlem2  23028  ivthlem3  23029  ovollb2lem  23063  ovoliunlem2  23078  ovolicc2lem3  23094  ismbf3d  23227  itg2seq  23315  itg2monolem1  23323  dvcnvrelem1  23584  itgsubst  23616  plypf1  23772  coeaddlem  23809  coemullem  23810  ulmcau  23953  abelth  23999  wilth  24597  ftalem2  24600  ftalem3  24601  muval1  24659  dvdssqf  24664  sqff1o  24708  chtub  24737  bposlem3  24811  lgsne0  24860  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  lgseisenlem1  24900  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2lem1  24909  lgsquad2lem2  24910  dchrisum0lem1  25005  pntlem3  25098  ex-natded5.8-2  26663  nmoub3i  27012  ubthlem1  27110  ubthlem2  27111  shsel1  27564  nmopub2tALT  28152  nmfnleub2  28169  lnconi  28276  eulerpartlemb  29757  dfon2lem4  30935  btwncomim  31290  nn0prpwlem  31487  ltflcei  32567  poimirlem9  32588  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  poimirlem24  32603  poimirlem29  32608  heicant  32614  mbfresfi  32626  itg2addnclem2  32632  itg2addnclem3  32633  incsequz  32714  heibor1lem  32778  atlelt  33742  1cvratex  33777  dalem3  33968  linepsubN  34056  pmapsub  34072  2llnma3r  34092  cdlemblem  34097  pmapjoin  34156  atmod1i1  34161  atmod1i2  34163  llnmod1i2  34164  lhpmcvr4N  34330  4atexlemnclw  34374  cdlemd3  34505  cdleme3g  34539  cdleme3h  34540  cdleme7d  34551  cdleme7ga  34553  cdleme21c  34633  cdleme35fnpq  34755  cdleme35f  34760  cdlemf1  34867  cdlemg4  34923  cdlemg6c  34926  cdlemg27a  34998  cdlemg33b0  35007  cdlemg33a  35012  cdlemk3  35139  dia2dimlem1  35371  dvheveccl  35419  dihord6apre  35563  dihord6b  35567  coprmdvdsb  36570  stoweid  38956  smonoord  39944  iccpartgt  39965  goldbachthlem2  39996  lighneallem2  40061  tgoldbach  40232  tgoldbachOLD  40239  upgrewlkle2  40808  pthdlem1  40972  crctcsh1wlkn0lem3  41015  nn0sumltlt  41921  dignn0flhalflem1  42207