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 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  5480  ordelinel  6420  nelrnfvne  7022  omass  8507  nnmass  8552  f1imaeng  8951  ssfi  9097  genpass  10920  adddir  11123  le2tri3i  11263  addsub12  11393  subdir  11571  ltaddsub  11611  leaddsub  11613  div12  11818  xmulass  13202  fldiv2  13781  modsubdir  13863  digit2  14159  muldivbinom2  14186  ccatass  14512  ccatw2s1cl  14548  repswcshw  14735  s3tpop  14832  absdiflt  15241  absdifle  15242  binomrisefac  15965  cos01gt0  16116  rpnnen2lem4  16142  rpnnen2lem7  16145  sadass  16398  lubub  18434  lubl  18435  symggrplem  18809  reslmhm2b  21006  cncrng  21343  ipcl  21588  ma1repveval  22515  mp2pm2mplem5  22754  opnneiss  23062  llyi  23418  nllyi  23419  cfiluweak  24238  cniccibl  25798  cnicciblnc  25800  ply1term  26165  explog  26559  logrec  26729  usgredgop  29243  usgr2v1e2w  29325  cusgrsizeinds  29526  clwwlknonex2  30184  4cycl2vnunb  30365  frrusgrord0lem  30414  frrusgrord0  30415  numclwwlk7  30466  lnocoi  30832  hvaddsubass  31116  hvmulcan2  31148  hhssabloilem  31336  hhssnv  31339  homco1  31876  homulass  31877  hoadddir  31879  hoaddsubass  31890  hosubsub4  31893  kbmul  32030  lnopmulsubi  32051  mdsl3  32391  cdj3lem2  32510  probmeasb  34587  signswmnd  34714  bnj563  34899  fineqvnttrclselem2  35278  fineqvnttrclselem3  35279  revpfxsfxrev  35310  lfuhgr2  35313  fnessex  36540  incsequz2  37946  ltrncnvatb  40394  jm2.17a  43198  lnrfgtr  43358  bdaybndex  43668  limsupvaluz2  45978  prsssprel  47730  dignnld  48845