Theorem stoic3 1772

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  opelopabt  5541  ordelinel  6486  nelrnfvne  7096  omass  8616  nnmass  8660  f1imaeng  9052  ssfi  9211  genpass  11046  adddir  11249  le2tri3i  11388  addsub12  11518  subdir  11694  ltaddsub  11734  leaddsub  11736  div12  11941  xmulass  13325  fldiv2  13897  modsubdir  13977  digit2  14271  muldivbinom2  14298  ccatass  14622  ccatw2s1cl  14658  repswcshw  14846  s3tpop  14944  absdiflt  15352  absdifle  15353  binomrisefac  16074  cos01gt0  16223  rpnnen2lem4  16249  rpnnen2lem7  16252  sadass  16504  lubub  18568  lubl  18569  symggrplem  18909  reslmhm2b  21070  cncrng  21418  ipcl  21668  ma1repveval  22592  mp2pm2mplem5  22831  opnneiss  23141  llyi  23497  nllyi  23498  cfiluweak  24319  cniccibl  25890  cnicciblnc  25892  ply1term  26257  explog  26650  logrec  26820  usgredgop  29201  usgr2v1e2w  29283  cusgrsizeinds  29484  clwwlknonex2  30137  4cycl2vnunb  30318  frrusgrord0lem  30367  frrusgrord0  30368  numclwwlk7  30419  lnocoi  30785  hvaddsubass  31069  hvmulcan2  31101  hhssabloilem  31289  hhssnv  31292  homco1  31829  homulass  31830  hoadddir  31832  hoaddsubass  31843  hosubsub4  31846  kbmul  31983  lnopmulsubi  32004  mdsl3  32344  cdj3lem2  32463  probmeasb  34411  signswmnd  34550  bnj563  34735  revpfxsfxrev  35099  lfuhgr2  35102  fnessex  36328  incsequz2  37735  ltrncnvatb  40120  jm2.17a  42948  lnrfgtr  43108  bdaybndex  43420  limsupvaluz2  45693  prsssprel  47412  dignnld  48452