Theorem stoic3 1803

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  opelopabt  5517  ordelinel  6465  nelrnfvne  7073  omass  8565  nnmass  8610  f1imaeng  9011  ssfi  9157  genpass  10994  adddir  11197  le2tri3i  11340  addsub12  11470  subdir  11648  ltaddsub  11688  leaddsub  11690  div12  11894  xmulass  13313  fldiv2  13894  modsubdir  13976  digit2  14272  muldivbinom2  14299  ccatass  14626  ccatw2s1cl  14662  repswcshw  14849  s3tpop  14946  absdiflt  15369  absdifle  15370  binomrisefac  16096  cos01gt0  16247  rpnnen2lem4  16273  rpnnen2lem7  16276  sadass  16529  lubub  18567  lubl  18568  symggrplem  18943  reslmhm2b  21153  cncrng  21512  ipcl  21752  ma1repveval  22697  mp2pm2mplem5  22936  opnneiss  23244  llyi  23600  nllyi  23601  cfiluweak  24420  cniccibl  25969  cnicciblnc  25971  ply1term  26330  explog  26725  logrec  26894  usgredgop  29461  usgr2v1e2w  29543  cusgrsizeinds  29743  clwwlknonex2  30401  4cycl2vnunb  30582  frrusgrord0lem  30631  frrusgrord0  30632  numclwwlk7  30683  lnocoi  31050  hvaddsubass  31334  hvmulcan2  31366  hhssabloilem  31554  hhssnv  31557  homco1  32094  homulass  32095  hoadddir  32097  hoaddsubass  32108  hosubsub4  32111  kbmul  32248  lnopmulsubi  32269  mdsl3  32609  cdj3lem2  32728  probmeasb  34765  signswmnd  34889  bnj563  35077  fineqvnttrclselem2  35468  fineqvnttrclselem3  35469  karddom  35507  kardsdom  35508  kardexen  35509  revpfxsfxrev  35540  lfuhgr2  35544  fnessex  36780  incsequz2  38323  ltrncnvatb  40837  jm2.17a  43614  lnrfgtr  43774  bdaybndex  44084  limsupvaluz2  46379  prsssprel  48161  dignnld  49303