Theorem stoic3 1770

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  opelopabt  5536  ordelinel  6473  nelrnfvne  7090  omass  8605  nnmass  8649  f1imaeng  9039  ssfi  9202  genpass  11038  adddir  11241  le2tri3i  11380  addsub12  11509  subdir  11684  ltaddsub  11724  leaddsub  11726  div12  11930  xmulass  13304  fldiv2  13864  modsubdir  13943  digit2  14236  muldivbinom2  14260  ccatass  14576  ccatw2s1cl  14612  repswcshw  14800  s3tpop  14898  absdiflt  15302  absdifle  15303  binomrisefac  16024  cos01gt0  16173  rpnnen2lem4  16199  rpnnen2lem7  16202  sadass  16451  lubub  18508  lubl  18509  symggrplem  18841  reslmhm2b  20944  cncrng  21321  ipcl  21570  ma1repveval  22491  mp2pm2mplem5  22730  opnneiss  23040  llyi  23396  nllyi  23397  cfiluweak  24218  cniccibl  25788  cnicciblnc  25790  ply1term  26156  explog  26546  logrec  26713  usgredgop  29001  usgr2v1e2w  29083  cusgrsizeinds  29284  clwwlknonex2  29937  4cycl2vnunb  30118  frrusgrord0lem  30167  frrusgrord0  30168  numclwwlk7  30219  lnocoi  30585  hvaddsubass  30869  hvmulcan2  30901  hhssabloilem  31089  hhssnv  31092  homco1  31629  homulass  31630  hoadddir  31632  hoaddsubass  31643  hosubsub4  31646  kbmul  31783  lnopmulsubi  31804  mdsl3  32144  cdj3lem2  32263  probmeasb  34055  signswmnd  34194  bnj563  34379  revpfxsfxrev  34730  lfuhgr2  34733  fnessex  35835  incsequz2  37227  ltrncnvatb  39615  jm2.17a  42384  lnrfgtr  42547  bdaybndex  42864  prsssprel  46830  dignnld  47727

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »