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  5470  ordelinel  6409  nelrnfvne  7010  omass  8495  nnmass  8539  f1imaeng  8936  ssfi  9082  genpass  10900  adddir  11103  le2tri3i  11243  addsub12  11373  subdir  11551  ltaddsub  11591  leaddsub  11593  div12  11798  xmulass  13186  fldiv2  13765  modsubdir  13847  digit2  14143  muldivbinom2  14170  ccatass  14496  ccatw2s1cl  14532  repswcshw  14719  s3tpop  14816  absdiflt  15225  absdifle  15226  binomrisefac  15949  cos01gt0  16100  rpnnen2lem4  16126  rpnnen2lem7  16129  sadass  16382  lubub  18417  lubl  18418  symggrplem  18792  reslmhm2b  20988  cncrng  21325  ipcl  21570  ma1repveval  22486  mp2pm2mplem5  22725  opnneiss  23033  llyi  23389  nllyi  23390  cfiluweak  24209  cniccibl  25769  cnicciblnc  25771  ply1term  26136  explog  26530  logrec  26700  usgredgop  29148  usgr2v1e2w  29230  cusgrsizeinds  29431  clwwlknonex2  30089  4cycl2vnunb  30270  frrusgrord0lem  30319  frrusgrord0  30320  numclwwlk7  30371  lnocoi  30737  hvaddsubass  31021  hvmulcan2  31053  hhssabloilem  31241  hhssnv  31244  homco1  31781  homulass  31782  hoadddir  31784  hoaddsubass  31795  hosubsub4  31798  kbmul  31935  lnopmulsubi  31956  mdsl3  32296  cdj3lem2  32415  probmeasb  34443  signswmnd  34570  bnj563  34755  fineqvnttrclselem2  35142  fineqvnttrclselem3  35143  revpfxsfxrev  35160  lfuhgr2  35163  fnessex  36390  incsequz2  37788  ltrncnvatb  40236  jm2.17a  43052  lnrfgtr  43212  bdaybndex  43523  limsupvaluz2  45835  prsssprel  47587  dignnld  48703