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  5481  ordelinel  6421  nelrnfvne  7024  omass  8509  nnmass  8554  f1imaeng  8955  ssfi  9101  genpass  10924  adddir  11127  le2tri3i  11267  addsub12  11397  subdir  11575  ltaddsub  11615  leaddsub  11617  div12  11822  xmulass  13206  fldiv2  13785  modsubdir  13867  digit2  14163  muldivbinom2  14190  ccatass  14516  ccatw2s1cl  14552  repswcshw  14739  s3tpop  14836  absdiflt  15245  absdifle  15246  binomrisefac  15969  cos01gt0  16120  rpnnen2lem4  16146  rpnnen2lem7  16149  sadass  16402  lubub  18438  lubl  18439  symggrplem  18813  reslmhm2b  21010  cncrng  21347  ipcl  21592  ma1repveval  22519  mp2pm2mplem5  22758  opnneiss  23066  llyi  23422  nllyi  23423  cfiluweak  24242  cniccibl  25802  cnicciblnc  25804  ply1term  26169  explog  26563  logrec  26733  usgredgop  29247  usgr2v1e2w  29329  cusgrsizeinds  29530  clwwlknonex2  30188  4cycl2vnunb  30369  frrusgrord0lem  30418  frrusgrord0  30419  numclwwlk7  30470  lnocoi  30836  hvaddsubass  31120  hvmulcan2  31152  hhssabloilem  31340  hhssnv  31343  homco1  31880  homulass  31881  hoadddir  31883  hoaddsubass  31894  hosubsub4  31897  kbmul  32034  lnopmulsubi  32055  mdsl3  32395  cdj3lem2  32514  probmeasb  34589  signswmnd  34716  bnj563  34901  fineqvnttrclselem2  35280  fineqvnttrclselem3  35281  revpfxsfxrev  35312  lfuhgr2  35315  fnessex  36542  incsequz2  37952  ltrncnvatb  40466  jm2.17a  43269  lnrfgtr  43429  bdaybndex  43739  limsupvaluz2  46049  prsssprel  47801  dignnld  48916