Theorem stoic3 1777

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  opelopabt  5419  ordelinel  6289  nelrnfvne  6845  omass  8206  nnmass  8250  f1imaeng  8569  genpass  10431  adddir  10632  le2tri3i  10770  addsub12  10899  subdir  11074  ltaddsub  11114  leaddsub  11116  div12  11320  xmulass  12681  fldiv2  13230  modsubdir  13309  digit2  13598  muldivbinom2  13624  ccatass  13942  ccatw2s1cl  13979  repswcshw  14174  s3tpop  14271  absdiflt  14677  absdifle  14678  binomrisefac  15396  cos01gt0  15544  rpnnen2lem4  15570  rpnnen2lem7  15573  sadass  15820  lubub  17729  lubl  17730  symggrplem  18049  reslmhm2b  19826  ipcl  20777  ma1repveval  21180  mp2pm2mplem5  21418  opnneiss  21726  llyi  22082  nllyi  22083  cfiluweak  22904  cniccibl  24441  ply1term  24794  explog  25177  logrec  25341  usgredgop  26955  usgr2v1e2w  27034  cusgrsizeinds  27234  clwwlknonex2  27888  4cycl2vnunb  28069  frrusgrord0lem  28118  frrusgrord0  28119  numclwwlk7  28170  lnocoi  28534  hvaddsubass  28818  hvmulcan2  28850  hhssabloilem  29038  hhssnv  29041  homco1  29578  homulass  29579  hoadddir  29581  hoaddsubass  29592  hosubsub4  29595  kbmul  29732  lnopmulsubi  29753  mdsl3  30093  cdj3lem2  30212  probmeasb  31688  signswmnd  31827  bnj563  32014  revpfxsfxrev  32362  lfuhgr2  32365  fnessex  33694  cnicciblnc  34978  incsequz2  35039  ltrncnvatb  37289  jm2.17a  39577  lnrfgtr  39740  prsssprel  43670  dignnld  44683