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  5475  ordelinel  6410  nelrnfvne  7011  omass  8498  nnmass  8542  f1imaeng  8939  ssfi  9087  genpass  10903  adddir  11106  le2tri3i  11246  addsub12  11376  subdir  11554  ltaddsub  11594  leaddsub  11596  div12  11801  xmulass  13189  fldiv2  13765  modsubdir  13847  digit2  14143  muldivbinom2  14170  ccatass  14495  ccatw2s1cl  14531  repswcshw  14718  s3tpop  14816  absdiflt  15225  absdifle  15226  binomrisefac  15949  cos01gt0  16100  rpnnen2lem4  16126  rpnnen2lem7  16129  sadass  16382  lubub  18417  lubl  18418  symggrplem  18758  reslmhm2b  20958  cncrng  21295  ipcl  21540  ma1repveval  22456  mp2pm2mplem5  22695  opnneiss  23003  llyi  23359  nllyi  23360  cfiluweak  24180  cniccibl  25740  cnicciblnc  25742  ply1term  26107  explog  26501  logrec  26671  usgredgop  29119  usgr2v1e2w  29201  cusgrsizeinds  29402  clwwlknonex2  30057  4cycl2vnunb  30238  frrusgrord0lem  30287  frrusgrord0  30288  numclwwlk7  30339  lnocoi  30705  hvaddsubass  30989  hvmulcan2  31021  hhssabloilem  31209  hhssnv  31212  homco1  31749  homulass  31750  hoadddir  31752  hoaddsubass  31763  hosubsub4  31766  kbmul  31903  lnopmulsubi  31924  mdsl3  32264  cdj3lem2  32383  probmeasb  34414  signswmnd  34541  bnj563  34726  fineqvnttrclselem2  35091  fineqvnttrclselem3  35092  revpfxsfxrev  35109  lfuhgr2  35112  fnessex  36340  incsequz2  37749  ltrncnvatb  40137  jm2.17a  42953  lnrfgtr  43113  bdaybndex  43424  limsupvaluz2  45739  prsssprel  47492  dignnld  48608