Theorem stoic3 1808

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  opelopabt  5505  ordelinel  6466  nelrnfvne  7077  omass  8588  nnmass  8633  f1imaeng  9041  ssfi  9188  genpass  11094  adddir  11297  le2tri3i  11440  addsub12  11570  subdir  11750  ltaddsub  11790  leaddsub  11792  div12  11996  xmulass  13417  fldiv2  14001  modsubdir  14083  digit2  14380  muldivbinom2  14407  ccatass  14734  ccatw2s1cl  14772  revpfxsfxrev  14917  repswcshw  14963  s3tpop  15060  absdiflt  15485  absdifle  15486  binomrisefac  16208  cos01gt0  16359  rpnnen2lem4  16385  rpnnen2lem7  16388  sadass  16641  lubub  18685  lubl  18686  symggrplem  19080  reslmhm2b  21329  cncrng  21699  ipcl  21939  ma1repveval  22886  mp2pm2mplem5  23128  opnneiss  23436  llyi  23793  nllyi  23794  cfiluweak  24613  cniccibl  26161  cnicciblnc  26163  ply1term  26522  explog  26922  logrec  27091  lfuhgr2  29727  usgredgop  29751  usgr2v1e2w  29833  cusgrsizeinds  30033  clwwlknonex2  30700  4cycl2vnunb  30891  frrusgrord0lem  30940  frrusgrord0  30941  numclwwlk7  30992  lnocoi  31359  hvaddsubass  31643  hvmulcan2  31675  hhssabloilem  31863  hhssnv  31866  homco1  32403  homulass  32404  hoadddir  32406  hoaddsubass  32417  hosubsub4  32420  kbmul  32557  lnopmulsubi  32578  mdsl3  32918  cdj3lem2  33037  probmeasb  35062  signswmnd  35186  bnj563  35374  fineqvnttrclselem2  35790  fineqvnttrclselem3  35791  karddom  35829  kardsdom  35830  kardexen  35831  nmulle  36966  fnessex  37134  incsequz2  38684  ltrncnvatb  41196  jm2.17a  43967  lnrfgtr  44122  bdaybndex  44432  limsupvaluz2  46748  prsssprel  48570  dignnld  49715