Theorem stoic3 1770

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

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

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 396  df-3an 1086

This theorem is referenced by:  opelopabt  5522  ordelinel  6455  nelrnfvne  7069  omass  8575  nnmass  8619  f1imaeng  9006  ssfi  9169  genpass  11000  adddir  11202  le2tri3i  11341  addsub12  11470  subdir  11645  ltaddsub  11685  leaddsub  11687  div12  11891  xmulass  13263  fldiv2  13823  modsubdir  13902  digit2  14196  muldivbinom2  14220  ccatass  14535  ccatw2s1cl  14571  repswcshw  14759  s3tpop  14857  absdiflt  15261  absdifle  15262  binomrisefac  15983  cos01gt0  16131  rpnnen2lem4  16157  rpnnen2lem7  16160  sadass  16409  lubub  18466  lubl  18467  symggrplem  18799  reslmhm2b  20892  ipcl  21494  ma1repveval  22395  mp2pm2mplem5  22634  opnneiss  22944  llyi  23300  nllyi  23301  cfiluweak  24122  cniccibl  25692  cnicciblnc  25694  ply1term  26058  explog  26444  logrec  26611  usgredgop  28899  usgr2v1e2w  28978  cusgrsizeinds  29178  clwwlknonex2  29831  4cycl2vnunb  30012  frrusgrord0lem  30061  frrusgrord0  30062  numclwwlk7  30113  lnocoi  30479  hvaddsubass  30763  hvmulcan2  30795  hhssabloilem  30983  hhssnv  30986  homco1  31523  homulass  31524  hoadddir  31526  hoaddsubass  31537  hosubsub4  31540  kbmul  31677  lnopmulsubi  31698  mdsl3  32038  cdj3lem2  32157  probmeasb  33918  signswmnd  34057  bnj563  34243  revpfxsfxrev  34595  lfuhgr2  34598  fnessex  35721  incsequz2  37107  ltrncnvatb  39499  jm2.17a  42188  lnrfgtr  42351  bdaybndex  42671  prsssprel  46641  dignnld  47477