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

Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086

This theorem is referenced by:  opelopabt  5384  ordelinel  6257  nelrnfvne  6822  omass  8189  nnmass  8233  f1imaeng  8552  genpass  10420  adddir  10621  le2tri3i  10759  addsub12  10888  subdir  11063  ltaddsub  11103  leaddsub  11105  div12  11309  xmulass  12668  fldiv2  13224  modsubdir  13303  digit2  13593  muldivbinom2  13619  ccatass  13933  ccatw2s1cl  13970  repswcshw  14165  s3tpop  14262  absdiflt  14669  absdifle  14670  binomrisefac  15388  cos01gt0  15536  rpnnen2lem4  15562  rpnnen2lem7  15565  sadass  15810  lubub  17721  lubl  17722  symggrplem  18041  reslmhm2b  19819  ipcl  20322  ma1repveval  21176  mp2pm2mplem5  21415  opnneiss  21723  llyi  22079  nllyi  22080  cfiluweak  22901  cniccibl  24444  cnicciblnc  24446  ply1term  24801  explog  25185  logrec  25349  usgredgop  26963  usgr2v1e2w  27042  cusgrsizeinds  27242  clwwlknonex2  27894  4cycl2vnunb  28075  frrusgrord0lem  28124  frrusgrord0  28125  numclwwlk7  28176  lnocoi  28540  hvaddsubass  28824  hvmulcan2  28856  hhssabloilem  29044  hhssnv  29047  homco1  29584  homulass  29585  hoadddir  29587  hoaddsubass  29598  hosubsub4  29601  kbmul  29738  lnopmulsubi  29759  mdsl3  30099  cdj3lem2  30218  probmeasb  31798  signswmnd  31937  bnj563  32124  revpfxsfxrev  32475  lfuhgr2  32478  fnessex  33807  incsequz2  35187  ltrncnvatb  37434  jm2.17a  39901  lnrfgtr  40064  prsssprel  44005  dignnld  45017