Theorem stoic3 1779

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 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  opelopabt  5445  ordelinel  6364  nelrnfvne  6955  omass  8411  nnmass  8455  f1imaeng  8800  ssfi  8956  genpass  10765  adddir  10966  le2tri3i  11105  addsub12  11234  subdir  11409  ltaddsub  11449  leaddsub  11451  div12  11655  xmulass  13021  fldiv2  13581  modsubdir  13660  digit2  13951  muldivbinom2  13977  ccatass  14293  ccatw2s1cl  14330  repswcshw  14525  s3tpop  14622  absdiflt  15029  absdifle  15030  binomrisefac  15752  cos01gt0  15900  rpnnen2lem4  15926  rpnnen2lem7  15929  sadass  16178  lubub  18229  lubl  18230  symggrplem  18523  reslmhm2b  20316  ipcl  20838  ma1repveval  21720  mp2pm2mplem5  21959  opnneiss  22269  llyi  22625  nllyi  22626  cfiluweak  23447  cniccibl  25005  cnicciblnc  25007  ply1term  25365  explog  25749  logrec  25913  usgredgop  27540  usgr2v1e2w  27619  cusgrsizeinds  27819  clwwlknonex2  28473  4cycl2vnunb  28654  frrusgrord0lem  28703  frrusgrord0  28704  numclwwlk7  28755  lnocoi  29119  hvaddsubass  29403  hvmulcan2  29435  hhssabloilem  29623  hhssnv  29626  homco1  30163  homulass  30164  hoadddir  30166  hoaddsubass  30177  hosubsub4  30180  kbmul  30317  lnopmulsubi  30338  mdsl3  30678  cdj3lem2  30797  probmeasb  32397  signswmnd  32536  bnj563  32723  revpfxsfxrev  33077  lfuhgr2  33080  fnessex  34535  incsequz2  35907  ltrncnvatb  38152  jm2.17a  40782  lnrfgtr  40945  prsssprel  44940  dignnld  45949