Theorem stoic3 1805

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 1126	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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

This theorem is used by:  opelopabt  5515  ordelinel  6464  nelrnfvne  7072  omass  8563  nnmass  8608  f1imaeng  9009  ssfi  9155  genpass  11000  adddir  11203  le2tri3i  11346  addsub12  11476  subdir  11654  ltaddsub  11694  leaddsub  11696  div12  11900  xmulass  13319  fldiv2  13901  modsubdir  13983  digit2  14279  muldivbinom2  14306  ccatass  14633  ccatw2s1cl  14669  repswcshw  14856  s3tpop  14953  absdiflt  15376  absdifle  15377  binomrisefac  16102  cos01gt0  16253  rpnnen2lem4  16279  rpnnen2lem7  16282  sadass  16535  lubub  18573  lubl  18574  symggrplem  18949  reslmhm2b  21186  cncrng  21554  ipcl  21794  ma1repveval  22739  mp2pm2mplem5  22978  opnneiss  23286  llyi  23642  nllyi  23643  cfiluweak  24462  cniccibl  26011  cnicciblnc  26013  ply1term  26372  explog  26770  logrec  26939  usgredgop  29531  usgr2v1e2w  29613  cusgrsizeinds  29813  clwwlknonex2  30471  4cycl2vnunb  30652  frrusgrord0lem  30701  frrusgrord0  30702  numclwwlk7  30753  lnocoi  31120  hvaddsubass  31404  hvmulcan2  31436  hhssabloilem  31624  hhssnv  31627  homco1  32164  homulass  32165  hoadddir  32167  hoaddsubass  32178  hosubsub4  32181  kbmul  32318  lnopmulsubi  32339  mdsl3  32679  cdj3lem2  32798  probmeasb  34829  signswmnd  34953  bnj563  35141  fineqvnttrclselem2  35543  fineqvnttrclselem3  35544  karddom  35582  kardsdom  35583  kardexen  35584  revpfxsfxrev  35615  lfuhgr2  35619  nmulle  36717  fnessex  36885  incsequz2  38428  ltrncnvatb  40940  jm2.17a  43715  lnrfgtr  43875  bdaybndex  44185  limsupvaluz2  46480  prsssprel  48265  dignnld  49411