Theorem stoic3 1774

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 579	. 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  5551  ordelinel  6496  nelrnfvne  7111  omass  8636  nnmass  8680  f1imaeng  9074  ssfi  9240  genpass  11078  adddir  11281  le2tri3i  11420  addsub12  11549  subdir  11724  ltaddsub  11764  leaddsub  11766  div12  11971  xmulass  13349  fldiv2  13912  modsubdir  13991  digit2  14285  muldivbinom2  14312  ccatass  14636  ccatw2s1cl  14672  repswcshw  14860  s3tpop  14958  absdiflt  15366  absdifle  15367  binomrisefac  16090  cos01gt0  16239  rpnnen2lem4  16265  rpnnen2lem7  16268  sadass  16517  lubub  18581  lubl  18582  symggrplem  18919  reslmhm2b  21076  cncrng  21424  ipcl  21674  ma1repveval  22598  mp2pm2mplem5  22837  opnneiss  23147  llyi  23503  nllyi  23504  cfiluweak  24325  cniccibl  25896  cnicciblnc  25898  ply1term  26263  explog  26654  logrec  26824  usgredgop  29205  usgr2v1e2w  29287  cusgrsizeinds  29488  clwwlknonex2  30141  4cycl2vnunb  30322  frrusgrord0lem  30371  frrusgrord0  30372  numclwwlk7  30423  lnocoi  30789  hvaddsubass  31073  hvmulcan2  31105  hhssabloilem  31293  hhssnv  31296  homco1  31833  homulass  31834  hoadddir  31836  hoaddsubass  31847  hosubsub4  31850  kbmul  31987  lnopmulsubi  32008  mdsl3  32348  cdj3lem2  32467  probmeasb  34395  signswmnd  34534  bnj563  34719  revpfxsfxrev  35083  lfuhgr2  35086  fnessex  36312  incsequz2  37709  ltrncnvatb  40095  jm2.17a  42917  lnrfgtr  43077  bdaybndex  43393  prsssprel  47362  dignnld  48337