Theorem mpand 691

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 690	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  692  mp2and  695  ecase2dOLD  1027  disjss3  5077  sotri2  6031  fpropnf1  7134  ovig  7410  orduniorsuc  7665  omopth2  8391  frfi  9020  ordunifi  9025  finsschain  9087  cantnfp1lem3  9399  cantnfp1  9400  p1le  11803  nnge1  11984  zltp1le  12353  gtndiv  12380  uzss  12587  eluzadd  12595  uzm1  12598  addlelt  12826  xrre2  12886  xrre3  12887  xrmaxlt  12897  xrmaxle  12899  xrsupsslem  13023  xrub  13028  supxrunb1  13035  zltaddlt1le  13219  nn0p1elfzo  13411  elfzoext  13425  flflp1  13508  ceile  13550  modfzo0difsn  13644  seqf1olem1  13743  leexp2r  13873  expnlbnd2  13930  facavg  13996  wrdred1hash  14245  ccat2s1fvw  14330  ccat2s1fvwOLD  14331  caubnd2  15050  limsupbnd1  15172  limsupbnd2  15173  rlim2lt  15187  rlim3  15188  o1co  15276  mulcn2  15286  cn1lem  15288  rlimo1  15307  climsqz  15331  climsqz2  15332  rlimsqzlem  15341  lo1le  15344  rlimno1  15346  climsup  15362  caucvgrlem2  15367  iseraltlem2  15375  iseralt  15377  fsumabs  15494  cvgcmp  15509  cvgcmpce  15511  isumltss  15541  cvgrat  15576  ruclem9  15928  ruclem12  15931  bitsfzolem  16122  bitsfzo  16123  sadcaddlem  16145  gcdzeq  16243  algcvgblem  16263  algcvga  16265  lcmdvdsb  16299  lcmftp  16322  coprm  16397  eulerthlem2  16464  pclem  16520  infpn2  16595  prmreclem1  16598  prmreclem4  16601  ramtlecl  16682  prmgaplem7  16739  initoeu2  17712  lubval  18055  lublecllem  18059  glbval  18068  joinle  18085  latmlem1  18168  odmulg  19144  efginvrel2  19314  pgpfac1lem5  19663  chfacfscmul0  21988  chfacfpmmul0  21992  1stccnp  22594  qustgplem  23253  imasdsf1olem  23507  bldisj  23532  xbln0  23548  prdsbl  23628  metss2lem  23648  stdbdxmet  23652  ngptgp  23773  nghmcn  23890  icoopnst  24083  iocopnst  24084  cnllycmp  24100  iscau3  24423  cmetcaulem  24433  iscmet3lem1  24436  bcthlem4  24472  ovollb2lem  24633  ovolicc2lem3  24664  voliunlem3  24697  volcn  24751  itg10a  24856  itg1ge0a  24857  bddiblnc  24987  dvcnvrelem1  25162  dvfsumrlim  25176  itgsubst  25194  ulmcn  25539  ulmdvlem3  25542  mtest  25544  tanord  25675  emcllem6  26131  ftalem2  26204  chtub  26341  fsumvma2  26343  vmasum  26345  chpchtsum  26348  bcmono  26406  bclbnd  26409  bposlem1  26413  bposlem5  26417  bposlem6  26418  lgsne0  26464  gausslemma2dlem1a  26494  chtppilim  26604  dchrisumlem3  26620  pntrsumbnd2  26696  pntlemf  26734  pntlem3  26738  pntleml  26740  upgr2pthnlp  28079  crctcshwlkn0lem3  28156  crctcshwlkn0lem5  28158  eupth2lems  28581  grpoidinvlem3  28847  grpoideu  28850  vacn  29035  blocni  29146  ubthlem2  29212  chscllem2  29979  lnconi  30374  pjnmopi  30489  atomli  30723  sumdmdlem2  30760  cdj3lem2b  30778  xraddge02  31058  fedgmullem1  31689  dfon2lem5  33742  dfon2lem6  33743  nosupno  33885  noinfno  33900  cgrcoml  34277  btwnconn2  34383  fvineqsneq  35562  pibt2  35567  ltflcei  35744  poimirlem2  35758  poimirlem18  35774  poimirlem22  35778  poimirlem23  35779  poimirlem26  35782  poimirlem29  35785  poimirlem30  35786  poimirlem32  35788  heicant  35791  mblfinlem3  35795  mblfinlem4  35796  itg2addnclem  35807  itg2addnc  35810  ftc1anclem6  35834  ftc1anc  35837  mettrifi  35894  geomcau  35896  equivbnd  35927  heibor1lem  35946  bfplem1  35959  bfplem2  35960  rrncmslem  35969  divrngidl  36165  lecmtN  37249  cvrletrN  37266  llnnleat  37506  lplnnle2at  37534  lvolnle3at  37575  dalem21  37687  cdlemblem  37786  osumcllem11N  37959  pexmidlem8N  37970  lhpmcvr4N  38019  cdleme32b  38435  cdleme35fnpq  38442  cdleme48bw  38495  cdlemf1  38554  cdlemg2fv2  38593  cdlemg7fvbwN  38600  cdlemg27b  38689  tendoeq2  38767  dia2dimlem1  39057  dihord6apre  39249  dihord5apre  39255  dihglbcpreN  39293  dochnel2  39385  dihjat1lem  39421  dochexmidlem8  39460  mapdordlem2  39630  3cubeslem1  40486  iscard5  41103  frege124d  41322  mnringmulrcld  41799  climinf  43101  2ffzoeq  44772  iccpartlt  44828  lighneallem2  45010  bgoldbtbndlem3  45211  bgoldbtbndlem4  45212  tgoldbach  45221  fllog2  45866  dignn0ldlem  45900