Theorem stoic3 1776

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  5487  ordelinel  6423  nelrnfvne  7031  omass  8521  nnmass  8565  f1imaeng  8962  ssfi  9114  genpass  10938  adddir  11141  le2tri3i  11280  addsub12  11410  subdir  11588  ltaddsub  11628  leaddsub  11630  div12  11835  xmulass  13223  fldiv2  13799  modsubdir  13881  digit2  14177  muldivbinom2  14204  ccatass  14529  ccatw2s1cl  14565  repswcshw  14753  s3tpop  14851  absdiflt  15260  absdifle  15261  binomrisefac  15984  cos01gt0  16135  rpnnen2lem4  16161  rpnnen2lem7  16164  sadass  16417  lubub  18452  lubl  18453  symggrplem  18793  reslmhm2b  20993  cncrng  21330  ipcl  21575  ma1repveval  22491  mp2pm2mplem5  22730  opnneiss  23038  llyi  23394  nllyi  23395  cfiluweak  24215  cniccibl  25775  cnicciblnc  25777  ply1term  26142  explog  26536  logrec  26706  usgredgop  29150  usgr2v1e2w  29232  cusgrsizeinds  29433  clwwlknonex2  30088  4cycl2vnunb  30269  frrusgrord0lem  30318  frrusgrord0  30319  numclwwlk7  30370  lnocoi  30736  hvaddsubass  31020  hvmulcan2  31052  hhssabloilem  31240  hhssnv  31243  homco1  31780  homulass  31781  hoadddir  31783  hoaddsubass  31794  hosubsub4  31797  kbmul  31934  lnopmulsubi  31955  mdsl3  32295  cdj3lem2  32414  probmeasb  34414  signswmnd  34541  bnj563  34726  revpfxsfxrev  35096  lfuhgr2  35099  fnessex  36327  incsequz2  37736  ltrncnvatb  40125  jm2.17a  42942  lnrfgtr  43102  bdaybndex  43413  limsupvaluz2  45729  prsssprel  47482  dignnld  48585