Theorem stoic3 1778

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 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 1089

This theorem is referenced by:  opelopabt  5532  ordelinel  6465  nelrnfvne  7079  omass  8582  nnmass  8626  f1imaeng  9012  ssfi  9175  genpass  11006  adddir  11209  le2tri3i  11348  addsub12  11477  subdir  11652  ltaddsub  11692  leaddsub  11694  div12  11898  xmulass  13270  fldiv2  13830  modsubdir  13909  digit2  14203  muldivbinom2  14227  ccatass  14542  ccatw2s1cl  14578  repswcshw  14766  s3tpop  14864  absdiflt  15268  absdifle  15269  binomrisefac  15990  cos01gt0  16138  rpnnen2lem4  16164  rpnnen2lem7  16167  sadass  16416  lubub  18468  lubl  18469  symggrplem  18801  reslmhm2b  20809  ipcl  21405  ma1repveval  22293  mp2pm2mplem5  22532  opnneiss  22842  llyi  23198  nllyi  23199  cfiluweak  24020  cniccibl  25582  cnicciblnc  25584  ply1term  25942  explog  26326  logrec  26492  usgredgop  28685  usgr2v1e2w  28764  cusgrsizeinds  28964  clwwlknonex2  29617  4cycl2vnunb  29798  frrusgrord0lem  29847  frrusgrord0  29848  numclwwlk7  29899  lnocoi  30265  hvaddsubass  30549  hvmulcan2  30581  hhssabloilem  30769  hhssnv  30772  homco1  31309  homulass  31310  hoadddir  31312  hoaddsubass  31323  hosubsub4  31326  kbmul  31463  lnopmulsubi  31484  mdsl3  31824  cdj3lem2  31943  probmeasb  33715  signswmnd  33854  bnj563  34040  revpfxsfxrev  34392  lfuhgr2  34395  fnessex  35534  incsequz2  36920  ltrncnvatb  39312  jm2.17a  42001  lnrfgtr  42164  bdaybndex  42484  prsssprel  46455  dignnld  47377