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  5482  ordelinel  6422  nelrnfvne  7025  omass  8510  nnmass  8555  f1imaeng  8956  ssfi  9102  genpass  10927  adddir  11130  le2tri3i  11271  addsub12  11401  subdir  11579  ltaddsub  11619  leaddsub  11621  div12  11826  xmulass  13234  fldiv2  13815  modsubdir  13897  digit2  14193  muldivbinom2  14220  ccatass  14546  ccatw2s1cl  14582  repswcshw  14769  s3tpop  14866  absdiflt  15275  absdifle  15276  binomrisefac  16002  cos01gt0  16153  rpnnen2lem4  16179  rpnnen2lem7  16182  sadass  16435  lubub  18472  lubl  18473  symggrplem  18847  reslmhm2b  21045  cncrng  21382  ipcl  21627  ma1repveval  22550  mp2pm2mplem5  22789  opnneiss  23097  llyi  23453  nllyi  23454  cfiluweak  24273  cniccibl  25822  cnicciblnc  25824  ply1term  26183  explog  26575  logrec  26744  usgredgop  29257  usgr2v1e2w  29339  cusgrsizeinds  29540  clwwlknonex2  30198  4cycl2vnunb  30379  frrusgrord0lem  30428  frrusgrord0  30429  numclwwlk7  30480  lnocoi  30847  hvaddsubass  31131  hvmulcan2  31163  hhssabloilem  31351  hhssnv  31354  homco1  31891  homulass  31892  hoadddir  31894  hoaddsubass  31905  hosubsub4  31908  kbmul  32045  lnopmulsubi  32066  mdsl3  32406  cdj3lem2  32525  probmeasb  34594  signswmnd  34721  bnj563  34906  fineqvnttrclselem2  35286  fineqvnttrclselem3  35287  revpfxsfxrev  35318  lfuhgr2  35321  fnessex  36548  incsequz2  38088  ltrncnvatb  40602  jm2.17a  43410  lnrfgtr  43570  bdaybndex  43880  limsupvaluz2  46188  prsssprel  47964  dignnld  49095