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  5492  ordelinel  6435  nelrnfvne  7049  omass  8544  nnmass  8588  f1imaeng  8985  ssfi  9137  genpass  10962  adddir  11165  le2tri3i  11304  addsub12  11434  subdir  11612  ltaddsub  11652  leaddsub  11654  div12  11859  xmulass  13247  fldiv2  13823  modsubdir  13905  digit2  14201  muldivbinom2  14228  ccatass  14553  ccatw2s1cl  14589  repswcshw  14777  s3tpop  14875  absdiflt  15284  absdifle  15285  binomrisefac  16008  cos01gt0  16159  rpnnen2lem4  16185  rpnnen2lem7  16188  sadass  16441  lubub  18470  lubl  18471  symggrplem  18811  reslmhm2b  20961  cncrng  21300  ipcl  21542  ma1repveval  22458  mp2pm2mplem5  22697  opnneiss  23005  llyi  23361  nllyi  23362  cfiluweak  24182  cniccibl  25742  cnicciblnc  25744  ply1term  26109  explog  26503  logrec  26673  usgredgop  29097  usgr2v1e2w  29179  cusgrsizeinds  29380  clwwlknonex2  30038  4cycl2vnunb  30219  frrusgrord0lem  30268  frrusgrord0  30269  numclwwlk7  30320  lnocoi  30686  hvaddsubass  30970  hvmulcan2  31002  hhssabloilem  31190  hhssnv  31193  homco1  31730  homulass  31731  hoadddir  31733  hoaddsubass  31744  hosubsub4  31747  kbmul  31884  lnopmulsubi  31905  mdsl3  32245  cdj3lem2  32364  probmeasb  34421  signswmnd  34548  bnj563  34733  revpfxsfxrev  35103  lfuhgr2  35106  fnessex  36334  incsequz2  37743  ltrncnvatb  40132  jm2.17a  42949  lnrfgtr  43109  bdaybndex  43420  limsupvaluz2  45736  prsssprel  47489  dignnld  48592