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  5479  ordelinel  6419  nelrnfvne  7022  omass  8507  nnmass  8552  f1imaeng  8953  ssfi  9099  genpass  10922  adddir  11125  le2tri3i  11265  addsub12  11395  subdir  11573  ltaddsub  11613  leaddsub  11615  div12  11820  xmulass  13204  fldiv2  13783  modsubdir  13865  digit2  14161  muldivbinom2  14188  ccatass  14514  ccatw2s1cl  14550  repswcshw  14737  s3tpop  14834  absdiflt  15243  absdifle  15244  binomrisefac  15967  cos01gt0  16118  rpnnen2lem4  16144  rpnnen2lem7  16147  sadass  16400  lubub  18436  lubl  18437  symggrplem  18811  reslmhm2b  21008  cncrng  21345  ipcl  21590  ma1repveval  22517  mp2pm2mplem5  22756  opnneiss  23064  llyi  23420  nllyi  23421  cfiluweak  24240  cniccibl  25800  cnicciblnc  25802  ply1term  26167  explog  26561  logrec  26731  usgredgop  29224  usgr2v1e2w  29306  cusgrsizeinds  29507  clwwlknonex2  30165  4cycl2vnunb  30346  frrusgrord0lem  30395  frrusgrord0  30396  numclwwlk7  30447  lnocoi  30813  hvaddsubass  31097  hvmulcan2  31129  hhssabloilem  31317  hhssnv  31320  homco1  31857  homulass  31858  hoadddir  31860  hoaddsubass  31871  hosubsub4  31874  kbmul  32011  lnopmulsubi  32032  mdsl3  32372  cdj3lem2  32491  probmeasb  34566  signswmnd  34693  bnj563  34878  fineqvnttrclselem2  35257  fineqvnttrclselem3  35258  revpfxsfxrev  35289  lfuhgr2  35292  fnessex  36519  incsequz2  37919  ltrncnvatb  40433  jm2.17a  43239  lnrfgtr  43399  bdaybndex  43709  limsupvaluz2  46019  prsssprel  47771  dignnld  48886