Theorem stoic3 1776

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  opelopabt  5422  ordelinel  6292  nelrnfvne  6848  omass  8209  nnmass  8253  f1imaeng  8572  genpass  10434  adddir  10635  le2tri3i  10773  addsub12  10902  subdir  11077  ltaddsub  11117  leaddsub  11119  div12  11323  xmulass  12683  fldiv2  13232  modsubdir  13311  digit2  13600  muldivbinom2  13626  ccatass  13945  ccatw2s1cl  13982  repswcshw  14177  s3tpop  14274  absdiflt  14680  absdifle  14681  binomrisefac  15399  cos01gt0  15547  rpnnen2lem4  15573  rpnnen2lem7  15576  sadass  15823  lubub  17732  lubl  17733  symggrplem  18052  reslmhm2b  19829  ipcl  20780  ma1repveval  21183  mp2pm2mplem5  21421  opnneiss  21729  llyi  22085  nllyi  22086  cfiluweak  22907  cniccibl  24444  ply1term  24797  explog  25180  logrec  25344  usgredgop  26958  usgr2v1e2w  27037  cusgrsizeinds  27237  clwwlknonex2  27891  4cycl2vnunb  28072  frrusgrord0lem  28121  frrusgrord0  28122  numclwwlk7  28173  lnocoi  28537  hvaddsubass  28821  hvmulcan2  28853  hhssabloilem  29041  hhssnv  29044  homco1  29581  homulass  29582  hoadddir  29584  hoaddsubass  29595  hosubsub4  29598  kbmul  29735  lnopmulsubi  29756  mdsl3  30096  cdj3lem2  30215  probmeasb  31692  signswmnd  31831  bnj563  32018  revpfxsfxrev  32366  lfuhgr2  32369  fnessex  33698  cnicciblnc  34967  incsequz2  35028  ltrncnvatb  37278  jm2.17a  39563  lnrfgtr  39726  prsssprel  43657  dignnld  44670