Theorem stoic3 1809

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  opelopabt  5503  ordelinel  6456  nelrnfvne  7066  omass  8567  nnmass  8612  f1imaeng  9020  ssfi  9167  genpass  11051  adddir  11254  le2tri3i  11397  addsub12  11527  subdir  11705  ltaddsub  11745  leaddsub  11747  div12  11951  xmulass  13372  fldiv2  13955  modsubdir  14037  digit2  14333  muldivbinom2  14360  ccatass  14687  ccatw2s1cl  14725  revpfxsfxrev  14870  repswcshw  14916  s3tpop  15013  absdiflt  15438  absdifle  15439  binomrisefac  16161  cos01gt0  16312  rpnnen2lem4  16338  rpnnen2lem7  16341  sadass  16594  lubub  18632  lubl  18633  symggrplem  19027  reslmhm2b  21276  cncrng  21646  ipcl  21886  ma1repveval  22833  mp2pm2mplem5  23075  opnneiss  23383  llyi  23740  nllyi  23741  cfiluweak  24560  cniccibl  26108  cnicciblnc  26110  ply1term  26469  explog  26871  logrec  27040  lfuhgr2  29646  usgredgop  29670  usgr2v1e2w  29752  cusgrsizeinds  29952  clwwlknonex2  30619  4cycl2vnunb  30810  frrusgrord0lem  30859  frrusgrord0  30860  numclwwlk7  30911  lnocoi  31278  hvaddsubass  31562  hvmulcan2  31594  hhssabloilem  31782  hhssnv  31785  homco1  32322  homulass  32323  hoadddir  32325  hoaddsubass  32336  hosubsub4  32339  kbmul  32476  lnopmulsubi  32497  mdsl3  32837  cdj3lem2  32956  probmeasb  34982  signswmnd  35106  bnj563  35294  fineqvnttrclselem2  35709  fineqvnttrclselem3  35710  karddom  35748  kardsdom  35749  kardexen  35750  nmulle  36882  fnessex  37050  incsequz2  38597  ltrncnvatb  41109  jm2.17a  43899  lnrfgtr  44059  bdaybndex  44369  limsupvaluz2  46664  prsssprel  48486  dignnld  49631