Theorem stoic3 1809

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 592	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)
4	3	3impa 1127	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  opelopabt  5510  ordelinel  6481  nelrnfvne  7098  omass  8613  nnmass  8658  f1imaeng  9066  ssfi  9213  genpass  11118  adddir  11321  le2tri3i  11464  addsub12  11594  subdir  11774  ltaddsub  11814  leaddsub  11816  div12  12020  xmulass  13441  fldiv2  14025  modsubdir  14107  digit2  14404  muldivbinom2  14431  ccatass  14758  ccatw2s1cl  14797  revpfxsfxrev  14942  repswcshw  14988  s3tpop  15086  absdiflt  15511  absdifle  15512  binomrisefac  16234  cos01gt0  16385  rpnnen2lem4  16411  rpnnen2lem7  16414  sadass  16667  lubub  18711  lubl  18712  symggrplem  19106  reslmhm2b  21356  cncrng  21726  ipcl  21966  ma1repveval  22913  mp2pm2mplem5  23155  opnneiss  23463  llyi  23820  nllyi  23821  cfiluweak  24640  cniccibl  26188  cnicciblnc  26190  ply1term  26549  explog  26949  logrec  27118  lfuhgr2  29754  usgredgop  29778  usgr2v1e2w  29860  cusgrsizeinds  30060  clwwlknonex2  30727  4cycl2vnunb  30918  frrusgrord0lem  30967  frrusgrord0  30968  numclwwlk7  31019  lnocoi  31386  hvaddsubass  31670  hvmulcan2  31702  hhssabloilem  31890  hhssnv  31893  homco1  32430  homulass  32431  hoadddir  32433  hoaddsubass  32444  hosubsub4  32447  kbmul  32584  lnopmulsubi  32605  mdsl3  32945  cdj3lem2  33064  probmeasb  35129  signswmnd  35253  bnj563  35441  fineqvnttrclselem2  35889  fineqvnttrclselem3  35890  karddom  35928  kardsdom  35929  kardexen  35930  j0ltaleph  36007  nmulle  37143  fnessex  37311  incsequz2  38874  ltrncnvatb  41386  jm2.17a  44158  lnrfgtr  44312  bdaybndex  44622  limsupvaluz2  46951  prsssprel  48773  dignnld  49918