Theorem mpand 692

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 691	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 206  df-an 396

This theorem is referenced by:  mpani  693  mp2and  696  ecase2dOLD  1028  disjss3  5147  sotri2  6130  fpropnf1  7269  ovig  7557  orduniorsuc  7822  omopth2  8590  onomeneq  9234  frfi  9294  ordunifi  9299  finsschain  9365  cantnfp1lem3  9681  cantnfp1  9682  p1le  12066  nnge1  12247  zltp1le  12619  gtndiv  12646  uzss  12852  eluzaddOLD  12864  uzm1  12867  addlelt  13095  xrre2  13156  xrre3  13157  xrmaxlt  13167  xrmaxle  13169  xrsupsslem  13293  xrub  13298  supxrunb1  13305  zltaddlt1le  13489  nn0p1elfzo  13682  elfzoext  13696  flflp1  13779  ceile  13821  modfzo0difsn  13915  seqf1olem1  14014  leexp2r  14146  expnlbnd2  14204  facavg  14268  wrdred1hash  14518  ccat2s1fvw  14595  caubnd2  15311  limsupbnd1  15433  limsupbnd2  15434  rlim2lt  15448  rlim3  15449  o1co  15537  mulcn2  15547  cn1lem  15549  rlimo1  15568  climsqz  15592  climsqz2  15593  rlimsqzlem  15602  lo1le  15605  rlimno1  15607  climsup  15623  caucvgrlem2  15628  iseraltlem2  15636  iseralt  15638  fsumabs  15754  cvgcmp  15769  cvgcmpce  15771  isumltss  15801  cvgrat  15836  ruclem9  16188  ruclem12  16191  bitsfzolem  16382  bitsfzo  16383  sadcaddlem  16405  gcdzeq  16501  algcvgblem  16521  algcvga  16523  lcmdvdsb  16557  lcmftp  16580  coprm  16655  eulerthlem2  16722  pclem  16778  infpn2  16853  prmreclem1  16856  prmreclem4  16859  ramtlecl  16940  prmgaplem7  16997  initoeu2  17976  lubval  18319  lublecllem  18323  glbval  18332  joinle  18349  latmlem1  18432  odmulg  19472  efginvrel2  19643  pgpfac1lem5  19997  chfacfscmul0  22680  chfacfpmmul0  22684  1stccnp  23286  qustgplem  23945  imasdsf1olem  24199  bldisj  24224  xbln0  24240  prdsbl  24320  metss2lem  24340  stdbdxmet  24344  ngptgp  24465  nghmcn  24582  icoopnst  24783  iocopnst  24784  cnllycmp  24802  iscau3  25126  cmetcaulem  25136  iscmet3lem1  25139  bcthlem4  25175  ovollb2lem  25337  ovolicc2lem3  25368  voliunlem3  25401  volcn  25455  itg10a  25560  itg1ge0a  25561  bddiblnc  25691  dvcnvrelem1  25870  dvfsumrlim  25886  itgsubst  25904  ulmcn  26250  ulmdvlem3  26253  mtest  26255  tanord  26387  emcllem6  26846  ftalem2  26919  chtub  27058  fsumvma2  27060  vmasum  27062  chpchtsum  27065  bcmono  27123  bclbnd  27126  bposlem1  27130  bposlem5  27134  bposlem6  27135  lgsne0  27181  gausslemma2dlem1a  27211  chtppilim  27321  dchrisumlem3  27337  pntrsumbnd2  27413  pntlemf  27451  pntlem3  27455  pntleml  27457  nosupno  27549  noinfno  27564  mulsproplem6  27934  mulsproplem7  27935  upgr2pthnlp  29422  crctcshwlkn0lem3  29499  crctcshwlkn0lem5  29501  eupth2lems  29924  grpoidinvlem3  30192  grpoideu  30195  vacn  30380  blocni  30491  ubthlem2  30557  chscllem2  31324  lnconi  31719  pjnmopi  31834  atomli  32068  sumdmdlem2  32105  cdj3lem2b  32123  xraddge02  32402  fedgmullem1  33168  dfon2lem5  35229  dfon2lem6  35230  cgrcoml  35438  btwnconn2  35544  fvineqsneq  36757  pibt2  36762  ltflcei  36940  poimirlem2  36954  poimirlem18  36970  poimirlem22  36974  poimirlem23  36975  poimirlem26  36978  poimirlem29  36981  poimirlem30  36982  poimirlem32  36984  heicant  36987  mblfinlem3  36991  mblfinlem4  36992  itg2addnclem  37003  itg2addnc  37006  ftc1anclem6  37030  ftc1anc  37033  mettrifi  37089  geomcau  37091  equivbnd  37122  heibor1lem  37141  bfplem1  37154  bfplem2  37155  rrncmslem  37164  divrngidl  37360  lecmtN  38590  cvrletrN  38607  llnnleat  38848  lplnnle2at  38876  lvolnle3at  38917  dalem21  39029  cdlemblem  39128  osumcllem11N  39301  pexmidlem8N  39312  lhpmcvr4N  39361  cdleme32b  39777  cdleme35fnpq  39784  cdleme48bw  39837  cdlemf1  39896  cdlemg2fv2  39935  cdlemg7fvbwN  39942  cdlemg27b  40031  tendoeq2  40109  dia2dimlem1  40399  dihord6apre  40591  dihord5apre  40597  dihglbcpreN  40635  dochnel2  40727  dihjat1lem  40763  dochexmidlem8  40802  mapdordlem2  40972  eqresfnbd  41521  3cubeslem1  41885  ordnexbtwnsuc  42480  naddcnfid2  42581  nadd2rabex  42599  iscard5  42750  frege124d  42975  mnringmulrcld  43450  climinf  44781  2ffzoeq  46495  iccpartlt  46551  lighneallem2  46733  bgoldbtbndlem3  46934  bgoldbtbndlem4  46935  tgoldbach  46944  fllog2  47416  dignn0ldlem  47450