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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  opelopabt  5494  ordelinel  6423  nelrnfvne  7033  omass  8532  nnmass  8576  f1imaeng  8961  ssfi  9124  genpass  10954  adddir  11155  le2tri3i  11294  addsub12  11423  subdir  11598  ltaddsub  11638  leaddsub  11640  div12  11844  xmulass  13216  fldiv2  13776  modsubdir  13855  digit2  14149  muldivbinom2  14173  ccatass  14488  ccatw2s1cl  14524  repswcshw  14712  s3tpop  14810  absdiflt  15214  absdifle  15215  binomrisefac  15936  cos01gt0  16084  rpnnen2lem4  16110  rpnnen2lem7  16113  sadass  16362  lubub  18414  lubl  18415  symggrplem  18708  reslmhm2b  20572  ipcl  21074  ma1repveval  21957  mp2pm2mplem5  22196  opnneiss  22506  llyi  22862  nllyi  22863  cfiluweak  23684  cniccibl  25242  cnicciblnc  25244  ply1term  25602  explog  25986  logrec  26150  usgredgop  28184  usgr2v1e2w  28263  cusgrsizeinds  28463  clwwlknonex2  29116  4cycl2vnunb  29297  frrusgrord0lem  29346  frrusgrord0  29347  numclwwlk7  29398  lnocoi  29762  hvaddsubass  30046  hvmulcan2  30078  hhssabloilem  30266  hhssnv  30269  homco1  30806  homulass  30807  hoadddir  30809  hoaddsubass  30820  hosubsub4  30823  kbmul  30960  lnopmulsubi  30981  mdsl3  31321  cdj3lem2  31440  probmeasb  33119  signswmnd  33258  bnj563  33444  revpfxsfxrev  33796  lfuhgr2  33799  fnessex  34894  incsequz2  36281  ltrncnvatb  38674  jm2.17a  41342  lnrfgtr  41505  bdaybndex  41825  prsssprel  45800  dignnld  46809