Theorem mpand 707

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpani  708  mp2and  711  disjss3  5107  sotri2  6129  fpropnf1  7265  ovig  7556  orduniorsuc  7825  resf1ext2b  7931  omopth2  8568  onomeneq  9197  frfi  9244  ordunifi  9249  finsschain  9315  cantnfp1lem3  9648  cantnfp1  9649  p1le  12059  nnge1  12263  zltp1le  12643  gtndiv  12672  uzss  12884  uzm1  12895  addlelt  13131  xrre2  13195  xrre3  13196  xrmaxlt  13206  xrmaxle  13208  xrsupsslem  13332  xrub  13337  supxrunb1  13344  zltaddlt1le  13531  nn0p1elfzo  13730  flflp1  13839  ceile  13881  modfzo0difsn  13978  seqf1olem1  14076  leexp2r  14209  expnlbnd2  14269  facavg  14336  wrdred1hash  14597  ccat2s1fvw  14675  caubnd2  15408  limsupbnd1  15532  limsupbnd2  15533  rlim2lt  15547  rlim3  15548  o1co  15636  mulcn2  15646  cn1lem  15648  rlimo1  15667  climsqz  15691  climsqz2  15692  rlimsqzlem  15699  lo1le  15702  rlimno1  15704  climsup  15720  caucvgrlem2  15725  iseraltlem2  15733  iseralt  15735  fsumabs  15852  cvgcmp  15867  cvgcmpce  15869  isumltss  15901  cvgrat  15936  ruclem9  16293  ruclem12  16296  bitsfzolem  16491  bitsfzo  16492  sadcaddlem  16514  gcdzeq  16609  algcvgblem  16634  algcvga  16636  lcmdvdsb  16670  lcmftp  16693  coprm  16769  eulerthlem2  16840  pclem  16897  infpn2  16972  prmreclem1  16975  prmreclem4  16978  ramtlecl  17059  prmgaplem7  17116  initoeu2  18072  lubval  18409  lublecllem  18413  glbval  18422  joinle  18439  latmlem1  18524  odmulg  19625  efginvrel2  19796  pgpfac1lem5  20150  chfacfscmul0  22994  chfacfpmmul0  22998  1stccnp  23598  qustgplem  24257  imasdsf1olem  24509  bldisj  24534  xbln0  24550  prdsbl  24627  metss2lem  24647  stdbdxmet  24651  ngptgp  24772  nghmcn  24881  icoopnst  25077  iocopnst  25078  cnllycmp  25094  iscau3  25416  cmetcaulem  25426  iscmet3lem1  25429  bcthlem4  25465  ovollb2lem  25626  ovolicc2lem3  25657  voliunlem3  25690  volcn  25744  itg10a  25848  itg1ge0a  25849  bddiblnc  25980  dvcnvrelem1  26155  dvfsumrlim  26169  itgsubst  26187  ulmcn  26538  ulmdvlem3  26541  mtest  26543  tanord  26679  emcllem6  27141  ftalem2  27214  chtub  27352  fsumvma2  27354  vmasum  27356  chpchtsum  27359  bcmono  27417  bclbnd  27420  bposlem1  27424  bposlem5  27428  bposlem6  27429  lgsne0  27475  gausslemma2dlem1a  27505  chtppilim  27615  dchrisumlem3  27631  pntrsumbnd2  27707  pntlemf  27745  pntlem3  27749  pntleml  27751  nosupno  27843  noinfno  27858  mulsproplem6  28290  mulsproplem7  28291  upgr2pthnlp  30047  crctcshwlkn0lem3  30127  crctcshwlkn0lem5  30129  eupth2lems  30555  grpoidinvlem3  30824  grpoideu  30827  vacn  31012  blocni  31123  ubthlem2  31189  chscllem2  31956  lnconi  32351  pjnmopi  32466  atomli  32700  sumdmdlem2  32737  cdj3lem2b  32755  xraddge02  33068  fedgmullem1  33985  dfon2lem5  36231  dfon2lem6  36232  cgrcoml  36442  btwnconn2  36548  fvineqsneq  38002  pibt2  38007  ltflcei  38203  poimirlem2  38217  poimirlem18  38233  poimirlem22  38237  poimirlem23  38238  poimirlem26  38241  poimirlem29  38244  poimirlem30  38245  poimirlem32  38247  heicant  38250  mblfinlem3  38254  mblfinlem4  38255  itg2addnclem  38266  itg2addnc  38269  ftc1anclem6  38293  ftc1anc  38296  mettrifi  38352  geomcau  38354  equivbnd  38385  heibor1lem  38404  bfplem1  38417  bfplem2  38418  rrncmslem  38427  divrngidl  38623  preuniqval  39091  lecmtN  39976  cvrletrN  39993  llnnleat  40233  lplnnle2at  40261  lvolnle3at  40302  dalem21  40414  cdlemblem  40513  osumcllem11N  40686  pexmidlem8N  40697  lhpmcvr4N  40746  cdleme32b  41162  cdleme35fnpq  41169  cdleme48bw  41222  cdlemf1  41281  cdlemg2fv2  41320  cdlemg7fvbwN  41327  cdlemg27b  41416  tendoeq2  41494  dia2dimlem1  41784  dihord6apre  41976  dihord5apre  41982  dihglbcpreN  42020  dochnel2  42112  dihjat1lem  42148  dochexmidlem8  42187  mapdordlem2  42357  eqresfnbd  42949  3cubeslem1  43363  ordnexbtwnsuc  43942  naddcnfid2  44043  nadd2rabex  44061  iscard5  44210  frege124d  44435  mnringmulrcld  44900  climinf  46270  2ffzoeq  48010  iccpartlt  48118  lighneallem2  48303  bgoldbtbndlem3  48517  bgoldbtbndlem4  48518  tgoldbach  48527  fllog2  49293  dignn0ldlem  49327