Theorem mpand 694

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 693	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  695  mp2and  698  ecase2dOLD  1031  disjss3  5165  sotri2  6161  fpropnf1  7304  ovig  7596  orduniorsuc  7866  omopth2  8640  onomeneq  9291  frfi  9349  ordunifi  9354  finsschain  9429  cantnfp1lem3  9749  cantnfp1  9750  p1le  12139  nnge1  12321  zltp1le  12693  gtndiv  12720  uzss  12926  eluzaddOLD  12938  uzm1  12941  addlelt  13171  xrre2  13232  xrre3  13233  xrmaxlt  13243  xrmaxle  13245  xrsupsslem  13369  xrub  13374  supxrunb1  13381  zltaddlt1le  13565  nn0p1elfzo  13759  elfzoext  13773  flflp1  13858  ceile  13900  modfzo0difsn  13994  seqf1olem1  14092  leexp2r  14224  expnlbnd2  14283  facavg  14350  wrdred1hash  14609  ccat2s1fvw  14686  caubnd2  15406  limsupbnd1  15528  limsupbnd2  15529  rlim2lt  15543  rlim3  15544  o1co  15632  mulcn2  15642  cn1lem  15644  rlimo1  15663  climsqz  15687  climsqz2  15688  rlimsqzlem  15697  lo1le  15700  rlimno1  15702  climsup  15718  caucvgrlem2  15723  iseraltlem2  15731  iseralt  15733  fsumabs  15849  cvgcmp  15864  cvgcmpce  15866  isumltss  15896  cvgrat  15931  ruclem9  16286  ruclem12  16289  bitsfzolem  16480  bitsfzo  16481  sadcaddlem  16503  gcdzeq  16599  algcvgblem  16624  algcvga  16626  lcmdvdsb  16660  lcmftp  16683  coprm  16758  eulerthlem2  16829  pclem  16885  infpn2  16960  prmreclem1  16963  prmreclem4  16966  ramtlecl  17047  prmgaplem7  17104  initoeu2  18083  lubval  18426  lublecllem  18430  glbval  18439  joinle  18456  latmlem1  18539  odmulg  19598  efginvrel2  19769  pgpfac1lem5  20123  chfacfscmul0  22885  chfacfpmmul0  22889  1stccnp  23491  qustgplem  24150  imasdsf1olem  24404  bldisj  24429  xbln0  24445  prdsbl  24525  metss2lem  24545  stdbdxmet  24549  ngptgp  24670  nghmcn  24787  icoopnst  24988  iocopnst  24989  cnllycmp  25007  iscau3  25331  cmetcaulem  25341  iscmet3lem1  25344  bcthlem4  25380  ovollb2lem  25542  ovolicc2lem3  25573  voliunlem3  25606  volcn  25660  itg10a  25765  itg1ge0a  25766  bddiblnc  25897  dvcnvrelem1  26076  dvfsumrlim  26092  itgsubst  26110  ulmcn  26460  ulmdvlem3  26463  mtest  26465  tanord  26598  emcllem6  27062  ftalem2  27135  chtub  27274  fsumvma2  27276  vmasum  27278  chpchtsum  27281  bcmono  27339  bclbnd  27342  bposlem1  27346  bposlem5  27350  bposlem6  27351  lgsne0  27397  gausslemma2dlem1a  27427  chtppilim  27537  dchrisumlem3  27553  pntrsumbnd2  27629  pntlemf  27667  pntlem3  27671  pntleml  27673  nosupno  27766  noinfno  27781  mulsproplem6  28165  mulsproplem7  28166  upgr2pthnlp  29768  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  eupth2lems  30270  grpoidinvlem3  30538  grpoideu  30541  vacn  30726  blocni  30837  ubthlem2  30903  chscllem2  31670  lnconi  32065  pjnmopi  32180  atomli  32414  sumdmdlem2  32451  cdj3lem2b  32469  xraddge02  32763  fedgmullem1  33642  dfon2lem5  35751  dfon2lem6  35752  cgrcoml  35960  btwnconn2  36066  fvineqsneq  37378  pibt2  37383  ltflcei  37568  poimirlem2  37582  poimirlem18  37598  poimirlem22  37602  poimirlem23  37603  poimirlem26  37606  poimirlem29  37609  poimirlem30  37610  poimirlem32  37612  heicant  37615  mblfinlem3  37619  mblfinlem4  37620  itg2addnclem  37631  itg2addnc  37634  ftc1anclem6  37658  ftc1anc  37661  mettrifi  37717  geomcau  37719  equivbnd  37750  heibor1lem  37769  bfplem1  37782  bfplem2  37783  rrncmslem  37792  divrngidl  37988  lecmtN  39212  cvrletrN  39229  llnnleat  39470  lplnnle2at  39498  lvolnle3at  39539  dalem21  39651  cdlemblem  39750  osumcllem11N  39923  pexmidlem8N  39934  lhpmcvr4N  39983  cdleme32b  40399  cdleme35fnpq  40406  cdleme48bw  40459  cdlemf1  40518  cdlemg2fv2  40557  cdlemg7fvbwN  40564  cdlemg27b  40653  tendoeq2  40731  dia2dimlem1  41021  dihord6apre  41213  dihord5apre  41219  dihglbcpreN  41257  dochnel2  41349  dihjat1lem  41385  dochexmidlem8  41424  mapdordlem2  41594  eqresfnbd  42227  3cubeslem1  42640  ordnexbtwnsuc  43229  naddcnfid2  43330  nadd2rabex  43348  iscard5  43498  frege124d  43723  mnringmulrcld  44197  climinf  45527  2ffzoeq  47242  iccpartlt  47298  lighneallem2  47480  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  tgoldbach  47691  fllog2  48302  dignn0ldlem  48336