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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  opelopabt  5487  ordelinel  6426  nelrnfvne  7029  omass  8515  nnmass  8560  f1imaeng  8961  ssfi  9107  genpass  10932  adddir  11135  le2tri3i  11276  addsub12  11406  subdir  11584  ltaddsub  11624  leaddsub  11626  div12  11831  xmulass  13239  fldiv2  13820  modsubdir  13902  digit2  14198  muldivbinom2  14225  ccatass  14551  ccatw2s1cl  14587  repswcshw  14774  s3tpop  14871  absdiflt  15280  absdifle  15281  binomrisefac  16007  cos01gt0  16158  rpnnen2lem4  16184  rpnnen2lem7  16187  sadass  16440  lubub  18477  lubl  18478  symggrplem  18852  reslmhm2b  21049  cncrng  21373  ipcl  21613  ma1repveval  22536  mp2pm2mplem5  22775  opnneiss  23083  llyi  23439  nllyi  23440  cfiluweak  24259  cniccibl  25808  cnicciblnc  25810  ply1term  26169  explog  26558  logrec  26727  usgredgop  29239  usgr2v1e2w  29321  cusgrsizeinds  29521  clwwlknonex2  30179  4cycl2vnunb  30360  frrusgrord0lem  30409  frrusgrord0  30410  numclwwlk7  30461  lnocoi  30828  hvaddsubass  31112  hvmulcan2  31144  hhssabloilem  31332  hhssnv  31335  homco1  31872  homulass  31873  hoadddir  31875  hoaddsubass  31886  hosubsub4  31889  kbmul  32026  lnopmulsubi  32047  mdsl3  32387  cdj3lem2  32506  probmeasb  34574  signswmnd  34701  bnj563  34886  fineqvnttrclselem2  35266  fineqvnttrclselem3  35267  revpfxsfxrev  35298  lfuhgr2  35301  fnessex  36528  incsequz2  38070  ltrncnvatb  40584  jm2.17a  43388  lnrfgtr  43548  bdaybndex  43858  limsupvaluz2  46166  prsssprel  47948  dignnld  49079