Theorem stoic3 1784

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  opelopabt  5477  ordelinel  6417  nelrnfvne  7022  omass  8509  nnmass  8554  f1imaeng  8955  ssfi  9101  genpass  10927  adddir  11130  le2tri3i  11271  addsub12  11401  subdir  11579  ltaddsub  11619  leaddsub  11621  div12  11826  xmulass  13234  fldiv2  13815  modsubdir  13897  digit2  14193  muldivbinom2  14220  ccatass  14546  ccatw2s1cl  14582  repswcshw  14769  s3tpop  14866  absdiflt  15275  absdifle  15276  binomrisefac  16002  cos01gt0  16153  rpnnen2lem4  16179  rpnnen2lem7  16182  sadass  16435  lubub  18472  lubl  18473  symggrplem  18847  reslmhm2b  21048  cncrng  21372  ipcl  21612  ma1repveval  22558  mp2pm2mplem5  22797  opnneiss  23105  llyi  23461  nllyi  23462  cfiluweak  24281  cniccibl  25830  cnicciblnc  25832  ply1term  26191  explog  26580  logrec  26749  usgredgop  29261  usgr2v1e2w  29343  cusgrsizeinds  29543  clwwlknonex2  30201  4cycl2vnunb  30382  frrusgrord0lem  30431  frrusgrord0  30432  numclwwlk7  30483  lnocoi  30850  hvaddsubass  31134  hvmulcan2  31166  hhssabloilem  31354  hhssnv  31357  homco1  31894  homulass  31895  hoadddir  31897  hoaddsubass  31908  hosubsub4  31911  kbmul  32048  lnopmulsubi  32069  mdsl3  32409  cdj3lem2  32528  probmeasb  34626  signswmnd  34753  bnj563  34941  fineqvnttrclselem2  35318  fineqvnttrclselem3  35319  revpfxsfxrev  35359  lfuhgr2  35362  fnessex  36589  incsequz2  38131  ltrncnvatb  40645  jm2.17a  43420  lnrfgtr  43580  bdaybndex  43890  limsupvaluz2  46195  prsssprel  47977  dignnld  49108