Theorem stoic3 1741

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  opelopabt  5016  ordelinel  5863  ordelinelOLD  5864  nelrnfvne  6393  omass  7705  nnmass  7749  f1imaeng  8057  genpass  9869  adddir  10069  le2tri3i  10205  addsub12  10332  subdir  10502  ltaddsub  10540  leaddsub  10542  div12  10745  xmulass  12155  fldiv2  12700  modsubdir  12779  digit2  13037  muldivbinom2  13087  ccatass  13406  ccatw2s1cl  13443  ccatw2s1lenOLD  13445  repswcshw  13604  s3tpop  13700  absdiflt  14101  absdifle  14102  binomrisefac  14817  cos01gt0  14965  rpnnen2lem4  14990  rpnnen2lem7  14993  sadass  15240  lubub  17166  lubl  17167  reslmhm2b  19102  ipcl  20026  ma1repveval  20425  mp2pm2mplem5  20663  opnneiss  20970  llyi  21325  nllyi  21326  cfiluweak  22146  cniccibl  23652  ply1term  24005  explog  24385  logrec  24546  usgredgop  26110  usgr2v1e2w  26189  cusgrsizeinds  26404  clwwlknonex2  27084  4cycl2vnunb  27270  frrusgrord0lem  27319  frrusgrord0  27320  numclwwlk7  27378  lnocoi  27740  hvaddsubass  28026  hvmulcan2  28058  hhssabloilem  28246  hhssnv  28249  homco1  28788  homulass  28789  hoadddir  28791  hoaddsubass  28802  hosubsub4  28805  kbmul  28942  lnopmulsubi  28963  mdsl3  29303  cdj3lem2  29422  probmeasb  30620  signswmnd  30762  bnj563  30939  fnessex  32466  cnicciblnc  33611  incsequz2  33675  ltrncnvatb  35742  jm2.17a  37844  lnrfgtr  38007  prsssprel  42063  dignnld  42722