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  5495  ordelinel  6438  nelrnfvne  7052  omass  8547  nnmass  8591  f1imaeng  8988  ssfi  9143  genpass  10969  adddir  11172  le2tri3i  11311  addsub12  11441  subdir  11619  ltaddsub  11659  leaddsub  11661  div12  11866  xmulass  13254  fldiv2  13830  modsubdir  13912  digit2  14208  muldivbinom2  14235  ccatass  14560  ccatw2s1cl  14596  repswcshw  14784  s3tpop  14882  absdiflt  15291  absdifle  15292  binomrisefac  16015  cos01gt0  16166  rpnnen2lem4  16192  rpnnen2lem7  16195  sadass  16448  lubub  18477  lubl  18478  symggrplem  18818  reslmhm2b  20968  cncrng  21307  ipcl  21549  ma1repveval  22465  mp2pm2mplem5  22704  opnneiss  23012  llyi  23368  nllyi  23369  cfiluweak  24189  cniccibl  25749  cnicciblnc  25751  ply1term  26116  explog  26510  logrec  26680  usgredgop  29104  usgr2v1e2w  29186  cusgrsizeinds  29387  clwwlknonex2  30045  4cycl2vnunb  30226  frrusgrord0lem  30275  frrusgrord0  30276  numclwwlk7  30327  lnocoi  30693  hvaddsubass  30977  hvmulcan2  31009  hhssabloilem  31197  hhssnv  31200  homco1  31737  homulass  31738  hoadddir  31740  hoaddsubass  31751  hosubsub4  31754  kbmul  31891  lnopmulsubi  31912  mdsl3  32252  cdj3lem2  32371  probmeasb  34428  signswmnd  34555  bnj563  34740  revpfxsfxrev  35110  lfuhgr2  35113  fnessex  36341  incsequz2  37750  ltrncnvatb  40139  jm2.17a  42956  lnrfgtr  43116  bdaybndex  43427  limsupvaluz2  45743  prsssprel  47493  dignnld  48596