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  5490  ordelinel  6430  nelrnfvne  7033  omass  8519  nnmass  8564  f1imaeng  8965  ssfi  9111  genpass  10934  adddir  11137  le2tri3i  11277  addsub12  11407  subdir  11585  ltaddsub  11625  leaddsub  11627  div12  11832  xmulass  13216  fldiv2  13795  modsubdir  13877  digit2  14173  muldivbinom2  14200  ccatass  14526  ccatw2s1cl  14562  repswcshw  14749  s3tpop  14846  absdiflt  15255  absdifle  15256  binomrisefac  15979  cos01gt0  16130  rpnnen2lem4  16156  rpnnen2lem7  16159  sadass  16412  lubub  18448  lubl  18449  symggrplem  18823  reslmhm2b  21023  cncrng  21360  ipcl  21605  ma1repveval  22532  mp2pm2mplem5  22771  opnneiss  23079  llyi  23435  nllyi  23436  cfiluweak  24255  cniccibl  25815  cnicciblnc  25817  ply1term  26182  explog  26576  logrec  26746  usgredgop  29261  usgr2v1e2w  29343  cusgrsizeinds  29544  clwwlknonex2  30202  4cycl2vnunb  30383  frrusgrord0lem  30432  frrusgrord0  30433  numclwwlk7  30484  lnocoi  30851  hvaddsubass  31135  hvmulcan2  31167  hhssabloilem  31355  hhssnv  31358  homco1  31895  homulass  31896  hoadddir  31898  hoaddsubass  31909  hosubsub4  31912  kbmul  32049  lnopmulsubi  32070  mdsl3  32410  cdj3lem2  32529  probmeasb  34614  signswmnd  34741  bnj563  34926  fineqvnttrclselem2  35306  fineqvnttrclselem3  35307  revpfxsfxrev  35338  lfuhgr2  35341  fnessex  36568  incsequz2  38029  ltrncnvatb  40543  jm2.17a  43346  lnrfgtr  43506  bdaybndex  43816  limsupvaluz2  46125  prsssprel  47877  dignnld  48992