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  5514  ordelinel  6465  nelrnfvne  7073  omass  8570  nnmass  8615  f1imaeng  9023  ssfi  9170  genpass  11021  adddir  11224  le2tri3i  11367  addsub12  11497  subdir  11675  ltaddsub  11715  leaddsub  11717  div12  11921  xmulass  13341  fldiv2  13924  modsubdir  14006  digit2  14302  muldivbinom2  14329  ccatass  14656  ccatw2s1cl  14694  revpfxsfxrev  14839  repswcshw  14885  s3tpop  14982  absdiflt  15407  absdifle  15408  binomrisefac  16132  cos01gt0  16283  rpnnen2lem4  16309  rpnnen2lem7  16312  sadass  16565  lubub  18603  lubl  18604  symggrplem  18994  reslmhm2b  21239  cncrng  21607  ipcl  21847  ma1repveval  22794  mp2pm2mplem5  23036  opnneiss  23344  llyi  23701  nllyi  23702  cfiluweak  24521  cniccibl  26070  cnicciblnc  26072  ply1term  26431  explog  26829  logrec  26998  lfuhgr2  29592  usgredgop  29616  usgr2v1e2w  29698  cusgrsizeinds  29898  clwwlknonex2  30565  4cycl2vnunb  30756  frrusgrord0lem  30805  frrusgrord0  30806  numclwwlk7  30857  lnocoi  31224  hvaddsubass  31508  hvmulcan2  31540  hhssabloilem  31728  hhssnv  31731  homco1  32268  homulass  32269  hoadddir  32271  hoaddsubass  32282  hosubsub4  32285  kbmul  32422  lnopmulsubi  32443  mdsl3  32783  cdj3lem2  32902  probmeasb  34928  signswmnd  35052  bnj563  35240  fineqvnttrclselem2  35635  fineqvnttrclselem3  35636  karddom  35674  kardsdom  35675  kardexen  35676  nmulle  36784  fnessex  36952  incsequz2  38486  ltrncnvatb  40998  jm2.17a  43788  lnrfgtr  43948  bdaybndex  44258  limsupvaluz2  46553  prsssprel  48375  dignnld  49520