MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  stoic3 Unicode version

Theorem stoic3 1609
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 external assumption, another follows, then 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
StepHypRef Expression
1 stoic3.1 . . 3
2 stoic3.2 . . 3
31, 2sylan 471 . 2
433impa 1191 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  opelopabt  4764  ordelinel  4981  nelrnfvne  6025  omass  7248  nnmass  7292  f1imaeng  7595  genpass  9408  adddir  9608  le2tri3i  9735  addsub12  9856  subdir  10016  ltaddsub  10051  leaddsub  10053  div12  10254  xmulass  11508  fldiv2  11988  modsubdir  12055  digit2  12299  ccatass  12605  ccatw2s1len  12629  repswcshw  12780  absdiflt  13150  absdifle  13151  cos01gt0  13926  rpnnen2lem4  13951  rpnnen2lem7  13954  sadass  14121  lubub  15749  lubl  15750  reslmhm2b  17700  ipcl  18668  ma1repveval  19073  mp2pm2mplem5  19311  opnneiss  19619  llyi  19975  nllyi  19976  cfiluweak  20798  cniccibl  22247  ply1term  22601  explog  22978  logrec  23151  4cycl2vnunb  25017  numclwwlkovf2ex  25086  numclwwlk7  25114  issubgoi  25312  ablomul  25357  lnocoi  25672  hvaddsubass  25958  hvmulcan2  25990  hhssnv  26180  homco1  26720  homulass  26721  hoadddir  26723  hoaddsubass  26734  hosubsub4  26737  kbmul  26874  lnopmulsubi  26895  mdsl3  27235  cdj3lem2  27354  probmeasb  28369  signswmnd  28514  binomrisefac  29164  cnicciblnc  30086  fnessex  30164  incsequz2  30242  jm2.17a  30898  lnrfgtr  31069  ccatw2s1cl  32344  bnj563  33800  ltrncnvatb  35862
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator