Theorem stoic3 1872

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

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  opelopabt  5183  ordelinel  6039  nelrnfvne  6579  omass  7900  nnmass  7944  f1imaeng  8255  genpass  10119  adddir  10319  le2tri3i  10457  addsub12  10586  subdir  10756  ltaddsub  10794  leaddsub  10796  div12  10999  xmulass  12366  fldiv2  12915  modsubdir  12994  digit2  13251  muldivbinom2  13303  ccatass  13608  ccatw2s1cl  13646  ccatw2s1lenOLD  13648  repswcshw  13897  s3tpop  13994  absdiflt  14398  absdifle  14399  binomrisefac  15109  cos01gt0  15257  rpnnen2lem4  15282  rpnnen2lem7  15285  sadass  15528  lubub  17434  lubl  17435  reslmhm2b  19375  ipcl  20302  ma1repveval  20703  mp2pm2mplem5  20943  opnneiss  21251  llyi  21606  nllyi  21607  cfiluweak  22427  cniccibl  23948  ply1term  24301  explog  24681  logrec  24845  usgredgop  26406  usgr2v1e2w  26486  cusgrsizeinds  26702  clwwlknonex2  27449  4cycl2vnunb  27639  frrusgrord0lem  27688  frrusgrord0  27689  numclwwlk7  27776  lnocoi  28137  hvaddsubass  28423  hvmulcan2  28455  hhssabloilem  28643  hhssnv  28646  homco1  29185  homulass  29186  hoadddir  29188  hoaddsubass  29199  hosubsub4  29202  kbmul  29339  lnopmulsubi  29360  mdsl3  29700  cdj3lem2  29819  probmeasb  31009  signswmnd  31152  bnj563  31330  fnessex  32853  cnicciblnc  33969  incsequz2  34032  ltrncnvatb  36159  jm2.17a  38308  lnrfgtr  38471  prsssprel  42533  dignnld  43192