Theorem mpand 696

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 465	. 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃))
4	1, 3	mpan2d 695	1 ⊢ (𝜑 → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  mpani  697  mp2and  700  disjss3  5085  sotri2  6084  fpropnf1  7213  ovig  7504  orduniorsuc  7772  resf1ext2b  7877  omopth2  8510  onomeneq  9139  frfi  9186  ordunifi  9191  finsschain  9260  cantnfp1lem3  9590  cantnfp1  9591  p1le  11987  nnge1  12174  zltp1le  12542  gtndiv  12570  uzss  12775  uzm1  12786  addlelt  13022  xrre2  13086  xrre3  13087  xrmaxlt  13097  xrmaxle  13099  xrsupsslem  13223  xrub  13228  supxrunb1  13235  zltaddlt1le  13422  nn0p1elfzo  13619  flflp1  13728  ceile  13770  modfzo0difsn  13867  seqf1olem1  13965  leexp2r  14098  expnlbnd2  14158  facavg  14225  wrdred1hash  14485  ccat2s1fvw  14563  caubnd2  15282  limsupbnd1  15406  limsupbnd2  15407  rlim2lt  15421  rlim3  15422  o1co  15510  mulcn2  15520  cn1lem  15522  rlimo1  15541  climsqz  15565  climsqz2  15566  rlimsqzlem  15573  lo1le  15576  rlimno1  15578  climsup  15594  caucvgrlem2  15599  iseraltlem2  15607  iseralt  15609  fsumabs  15725  cvgcmp  15740  cvgcmpce  15742  isumltss  15772  cvgrat  15807  ruclem9  16164  ruclem12  16167  bitsfzolem  16362  bitsfzo  16363  sadcaddlem  16385  gcdzeq  16480  algcvgblem  16505  algcvga  16507  lcmdvdsb  16541  lcmftp  16564  coprm  16639  eulerthlem2  16710  pclem  16767  infpn2  16842  prmreclem1  16845  prmreclem4  16848  ramtlecl  16929  prmgaplem7  16986  initoeu2  17941  lubval  18278  lublecllem  18282  glbval  18291  joinle  18308  latmlem1  18393  odmulg  19489  efginvrel2  19660  pgpfac1lem5  20014  chfacfscmul0  22801  chfacfpmmul0  22805  1stccnp  23405  qustgplem  24064  imasdsf1olem  24316  bldisj  24341  xbln0  24357  prdsbl  24434  metss2lem  24454  stdbdxmet  24458  ngptgp  24579  nghmcn  24688  icoopnst  24884  iocopnst  24885  cnllycmp  24901  iscau3  25223  cmetcaulem  25233  iscmet3lem1  25236  bcthlem4  25272  ovollb2lem  25433  ovolicc2lem3  25464  voliunlem3  25497  volcn  25551  itg10a  25655  itg1ge0a  25656  bddiblnc  25787  dvcnvrelem1  25963  dvfsumrlim  25979  itgsubst  25997  ulmcn  26348  ulmdvlem3  26351  mtest  26353  tanord  26487  emcllem6  26951  ftalem2  27024  chtub  27163  fsumvma2  27165  vmasum  27167  chpchtsum  27170  bcmono  27228  bclbnd  27231  bposlem1  27235  bposlem5  27239  bposlem6  27240  lgsne0  27286  gausslemma2dlem1a  27316  chtppilim  27426  dchrisumlem3  27442  pntrsumbnd2  27518  pntlemf  27556  pntlem3  27560  pntleml  27562  nosupno  27655  noinfno  27670  mulsproplem6  28101  mulsproplem7  28102  upgr2pthnlp  29789  crctcshwlkn0lem3  29869  crctcshwlkn0lem5  29871  eupth2lems  30297  grpoidinvlem3  30566  grpoideu  30569  vacn  30754  blocni  30865  ubthlem2  30931  chscllem2  31698  lnconi  32093  pjnmopi  32208  atomli  32442  sumdmdlem2  32479  cdj3lem2b  32497  xraddge02  32820  fedgmullem1  33779  dfon2lem5  35973  dfon2lem6  35974  cgrcoml  36184  btwnconn2  36290  fvineqsneq  37724  pibt2  37729  ltflcei  37920  poimirlem2  37934  poimirlem18  37950  poimirlem22  37954  poimirlem23  37955  poimirlem26  37958  poimirlem29  37961  poimirlem30  37962  poimirlem32  37964  heicant  37967  mblfinlem3  37971  mblfinlem4  37972  itg2addnclem  37983  itg2addnc  37986  ftc1anclem6  38010  ftc1anc  38013  mettrifi  38069  geomcau  38071  equivbnd  38102  heibor1lem  38121  bfplem1  38134  bfplem2  38135  rrncmslem  38144  divrngidl  38340  preuniqval  38808  lecmtN  39693  cvrletrN  39710  llnnleat  39950  lplnnle2at  39978  lvolnle3at  40019  dalem21  40131  cdlemblem  40230  osumcllem11N  40403  pexmidlem8N  40414  lhpmcvr4N  40463  cdleme32b  40879  cdleme35fnpq  40886  cdleme48bw  40939  cdlemf1  40998  cdlemg2fv2  41037  cdlemg7fvbwN  41044  cdlemg27b  41133  tendoeq2  41211  dia2dimlem1  41501  dihord6apre  41693  dihord5apre  41699  dihglbcpreN  41737  dochnel2  41829  dihjat1lem  41865  dochexmidlem8  41904  mapdordlem2  42074  eqresfnbd  42665  3cubeslem1  43115  ordnexbtwnsuc  43698  naddcnfid2  43799  nadd2rabex  43817  iscard5  43966  frege124d  44191  mnringmulrcld  44658  climinf  46040  2ffzoeq  47761  iccpartlt  47858  lighneallem2  48040  bgoldbtbndlem3  48241  bgoldbtbndlem4  48242  tgoldbach  48251  fllog2  49002  dignn0ldlem  49036