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 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  5537  ordelinel  6485  nelrnfvne  7097  omass  8618  nnmass  8662  f1imaeng  9054  ssfi  9213  genpass  11049  adddir  11252  le2tri3i  11391  addsub12  11521  subdir  11697  ltaddsub  11737  leaddsub  11739  div12  11944  xmulass  13329  fldiv2  13901  modsubdir  13981  digit2  14275  muldivbinom2  14302  ccatass  14626  ccatw2s1cl  14662  repswcshw  14850  s3tpop  14948  absdiflt  15356  absdifle  15357  binomrisefac  16078  cos01gt0  16227  rpnnen2lem4  16253  rpnnen2lem7  16256  sadass  16508  lubub  18556  lubl  18557  symggrplem  18897  reslmhm2b  21053  cncrng  21401  ipcl  21651  ma1repveval  22577  mp2pm2mplem5  22816  opnneiss  23126  llyi  23482  nllyi  23483  cfiluweak  24304  cniccibl  25876  cnicciblnc  25878  ply1term  26243  explog  26636  logrec  26806  usgredgop  29187  usgr2v1e2w  29269  cusgrsizeinds  29470  clwwlknonex2  30128  4cycl2vnunb  30309  frrusgrord0lem  30358  frrusgrord0  30359  numclwwlk7  30410  lnocoi  30776  hvaddsubass  31060  hvmulcan2  31092  hhssabloilem  31280  hhssnv  31283  homco1  31820  homulass  31821  hoadddir  31823  hoaddsubass  31834  hosubsub4  31837  kbmul  31974  lnopmulsubi  31995  mdsl3  32335  cdj3lem2  32454  probmeasb  34432  signswmnd  34572  bnj563  34757  revpfxsfxrev  35121  lfuhgr2  35124  fnessex  36347  incsequz2  37756  ltrncnvatb  40140  jm2.17a  42972  lnrfgtr  43132  bdaybndex  43444  limsupvaluz2  45753  prsssprel  47475  dignnld  48524