Theorem mpand 708

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpand.1	⊢ (𝜑 → 𝜓)
mpand.2	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
mpand	⊢ (𝜑 → (𝜒 → 𝜃))

Proof of Theorem mpand

Step	Hyp	Ref	Expression
1		mpand.1	. 2 ⊢ (𝜑 → 𝜓)
2		mpand.2	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	ancomsd 471	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 707	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:  mpani  709  mp2and  712  disjss3  5101  sotri2  6117  fpropnf1  7259  ovig  7554  orduniorsuc  7824  resf1ext2b  7930  omopth2  8570  onomeneq  9207  frfi  9254  ordunifi  9259  finsschain  9326  cantnfp1lem3  9659  cantnfp1  9660  p1le  12131  nnge1  12335  zltp1le  12715  gtndiv  12745  uzss  12957  uzm1  12968  addlelt  13205  xrre2  13269  xrre3  13270  xrmaxlt  13280  xrmaxle  13282  xrsupsslem  13406  xrub  13411  supxrunb1  13418  zltaddlt1le  13605  nn0p1elfzo  13805  flflp1  13915  ceile  13957  modfzo0difsn  14054  seqf1olem1  14152  leexp2r  14285  expnlbnd2  14345  facavg  14412  wrdred1hash  14673  ccat2s1fvw  14753  caubnd2  15492  limsupbnd1  15616  limsupbnd2  15617  rlim2lt  15631  rlim3  15632  o1co  15720  mulcn2  15730  cn1lem  15732  rlimo1  15751  climsqz  15775  climsqz2  15776  rlimsqzlem  15783  lo1le  15786  rlimno1  15788  climsup  15804  caucvgrlem2  15809  iseraltlem2  15817  iseralt  15819  fsumabs  15935  cvgcmp  15950  cvgcmpce  15952  isumltss  15984  cvgrat  16019  ruclem9  16373  ruclem12  16376  bitsfzolem  16571  bitsfzo  16572  sadcaddlem  16594  gcdzeq  16689  algcvgblem  16714  algcvga  16716  lcmdvdsb  16750  lcmftp  16773  coprm  16849  eulerthlem2  16920  pclem  16977  infpn2  17052  prmreclem1  17055  prmreclem4  17058  ramtlecl  17139  prmgaplem7  17196  initoeu2  18152  lubval  18489  lublecllem  18493  glbval  18502  joinle  18519  latmlem1  18604  odmulg  19731  efginvrel2  19902  pgpfac1lem5  20256  chfacfscmul0  23137  chfacfpmmul0  23141  1stccnp  23742  qustgplem  24401  imasdsf1olem  24653  bldisj  24678  xbln0  24694  prdsbl  24771  metss2lem  24791  stdbdxmet  24795  ngptgp  24916  nghmcn  25025  icoopnst  25221  iocopnst  25222  cnllycmp  25238  iscau3  25560  cmetcaulem  25570  iscmet3lem1  25573  bcthlem4  25609  ovollb2lem  25770  ovolicc2lem3  25801  voliunlem3  25834  volcn  25888  itg10a  25992  itg1ge0a  25993  bddiblnc  26123  dvcnvrelem1  26298  dvfsumrlim  26312  itgsubst  26330  ulmcn  26689  ulmdvlem3  26692  mtest  26694  tanord  26829  emcllem6  27291  ftalem2  27364  chtub  27502  fsumvma2  27504  vmasum  27506  chpchtsum  27509  bcmono  27567  bclbnd  27570  bposlem1  27574  bposlem5  27578  bposlem6  27579  lgsne0  27625  gausslemma2dlem1a  27655  chtppilim  27765  dchrisumlem3  27781  pntrsumbnd2  27857  pntlemf  27895  pntlem3  27899  pntleml  27901  nosupno  27993  noinfno  28008  mulsproplem6  28440  mulsproplem7  28441  upgr2pthnlp  30251  crctcshwlkn0lem3  30334  crctcshwlkn0lem5  30336  eupth2lems  30772  grpoidinvlem3  31041  grpoideu  31044  vacn  31229  blocni  31340  ubthlem2  31406  chscllem2  32173  lnconi  32568  pjnmopi  32683  atomli  32917  sumdmdlem2  32954  cdj3lem2b  32972  xraddge02  33282  fedgmullem1  34194  dfon2lem5  36471  dfon2lem6  36472  cgrcoml  36683  btwnconn2  36789  fvineqsneq  38255  pibt2  38260  ltflcei  38451  poimirlem2  38460  poimirlem18  38476  poimirlem22  38480  poimirlem23  38481  poimirlem26  38484  poimirlem29  38487  poimirlem30  38488  poimirlem32  38490  heicant  38493  mblfinlem3  38497  mblfinlem4  38498  itg2addnclem  38509  itg2addnc  38512  ftc1anclem6  38536  ftc1anc  38539  mettrifi  38611  geomcau  38613  equivbnd  38644  heibor1lem  38663  bfplem1  38676  bfplem2  38677  rrncmslem  38686  divrngidl  38882  preuniqval  39348  lecmtN  40233  cvrletrN  40250  llnnleat  40490  lplnnle2at  40518  lvolnle3at  40559  dalem21  40671  cdlemblem  40770  osumcllem11N  40943  pexmidlem8N  40954  lhpmcvr4N  41003  cdleme32b  41419  cdleme35fnpq  41426  cdleme48bw  41479  cdlemf1  41538  cdlemg2fv2  41577  cdlemg7fvbwN  41584  cdlemg27b  41673  tendoeq2  41751  dia2dimlem1  42041  dihord6apre  42233  dihord5apre  42239  dihglbcpreN  42277  dochnel2  42369  dihjat1lem  42405  dochexmidlem8  42444  mapdordlem2  42614  eqresfnbd  43206  3cubeslem1  43633  ordnexbtwnsuc  44212  naddcnfid2  44313  nadd2rabex  44331  iscard5  44480  frege124d  44705  mnringmulrcld  45170  climinf  46540  2ffzoeq  48320  iccpartlt  48428  lighneallem2  48613  bgoldbtbndlem3  48827  bgoldbtbndlem4  48828  tgoldbach  48837  fllog2  49602  dignn0ldlem  49636