Theorem stoic3 1798

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 589	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)
4	3	3impa 1123	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  opelopabt  5504  ordelinel  6451  nelrnfvne  7060  omass  8551  nnmass  8596  f1imaeng  8997  ssfi  9143  genpass  10969  adddir  11172  le2tri3i  11315  addsub12  11445  subdir  11623  ltaddsub  11663  leaddsub  11665  div12  11869  xmulass  13292  fldiv2  13873  modsubdir  13955  digit2  14251  muldivbinom2  14278  ccatass  14604  ccatw2s1cl  14640  repswcshw  14827  s3tpop  14924  absdiflt  15347  absdifle  15348  binomrisefac  16074  cos01gt0  16225  rpnnen2lem4  16251  rpnnen2lem7  16254  sadass  16507  lubub  18545  lubl  18546  symggrplem  18920  reslmhm2b  21123  cncrng  21447  ipcl  21687  ma1repveval  22633  mp2pm2mplem5  22872  opnneiss  23180  llyi  23536  nllyi  23537  cfiluweak  24356  cniccibl  25905  cnicciblnc  25907  ply1term  26266  explog  26661  logrec  26830  usgredgop  29373  usgr2v1e2w  29455  cusgrsizeinds  29655  clwwlknonex2  30313  4cycl2vnunb  30494  frrusgrord0lem  30543  frrusgrord0  30544  numclwwlk7  30595  lnocoi  30962  hvaddsubass  31246  hvmulcan2  31278  hhssabloilem  31466  hhssnv  31469  homco1  32006  homulass  32007  hoadddir  32009  hoaddsubass  32020  hosubsub4  32023  kbmul  32160  lnopmulsubi  32181  mdsl3  32521  cdj3lem2  32640  probmeasb  34729  signswmnd  34853  bnj563  35041  fineqvnttrclselem2  35422  fineqvnttrclselem3  35423  revpfxsfxrev  35470  lfuhgr2  35474  fnessex  36711  incsequz2  38253  ltrncnvatb  40767  jm2.17a  43542  lnrfgtr  43702  bdaybndex  44012  limsupvaluz2  46317  prsssprel  48099  dignnld  49230