Theorem stoic3 1776

Description: Stoic logic Thema 3. Statement T3 of [Bobzien] p. 116-117 discusses Stoic logic Thema 3. "When from two (assemblies) a third follows, and from the one that follows (i.e., the third) together with another, external assumption, another follows, then that other follows from the first two and the externally co-assumed one. (Simp. Cael. 237.2-4)" (Contributed by David A. Wheeler, 17-Feb-2019.)

Hypotheses

Ref	Expression
stoic3.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
stoic3.2	⊢ ((𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
stoic3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Proof of Theorem stoic3

Step	Hyp	Ref	Expression
1		stoic3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		stoic3.2	. . 3 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
3	1, 2	sylan 580	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)
4	3	3impa 1109	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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  df-3an 1088

This theorem is referenced by:  opelopabt  5507  ordelinel  6454  nelrnfvne  7066  omass  8590  nnmass  8634  f1imaeng  9026  ssfi  9185  genpass  11021  adddir  11224  le2tri3i  11363  addsub12  11493  subdir  11669  ltaddsub  11709  leaddsub  11711  div12  11916  xmulass  13301  fldiv2  13876  modsubdir  13956  digit2  14252  muldivbinom2  14279  ccatass  14604  ccatw2s1cl  14640  repswcshw  14828  s3tpop  14926  absdiflt  15334  absdifle  15335  binomrisefac  16056  cos01gt0  16207  rpnnen2lem4  16233  rpnnen2lem7  16236  sadass  16488  lubub  18519  lubl  18520  symggrplem  18860  reslmhm2b  21010  cncrng  21349  ipcl  21591  ma1repveval  22507  mp2pm2mplem5  22746  opnneiss  23054  llyi  23410  nllyi  23411  cfiluweak  24231  cniccibl  25792  cnicciblnc  25794  ply1term  26159  explog  26553  logrec  26723  usgredgop  29095  usgr2v1e2w  29177  cusgrsizeinds  29378  clwwlknonex2  30036  4cycl2vnunb  30217  frrusgrord0lem  30266  frrusgrord0  30267  numclwwlk7  30318  lnocoi  30684  hvaddsubass  30968  hvmulcan2  31000  hhssabloilem  31188  hhssnv  31191  homco1  31728  homulass  31729  hoadddir  31731  hoaddsubass  31742  hosubsub4  31745  kbmul  31882  lnopmulsubi  31903  mdsl3  32243  cdj3lem2  32362  probmeasb  34408  signswmnd  34535  bnj563  34720  revpfxsfxrev  35084  lfuhgr2  35087  fnessex  36310  incsequz2  37719  ltrncnvatb  40103  jm2.17a  42931  lnrfgtr  43091  bdaybndex  43402  limsupvaluz2  45715  prsssprel  47450  dignnld  48531