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

Theorem stoic3 1692
 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 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 487 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜏)
433impa 1251 1 ((𝜑𝜓𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  opelopabt  4912  ordelinel  5742  ordelinelOLD  5743  nelrnfvne  6261  omass  7547  nnmass  7591  f1imaeng  7902  genpass  9710  adddir  9910  le2tri3i  10046  addsub12  10173  subdir  10343  ltaddsub  10381  leaddsub  10383  div12  10586  xmulass  11989  fldiv2  12522  modsubdir  12601  digit2  12859  muldivbinom2  12909  ccatass  13224  ccatw2s1len  13254  repswcshw  13409  s3tpop  13504  absdiflt  13905  absdifle  13906  binomrisefac  14612  cos01gt0  14760  rpnnen2lem4  14785  rpnnen2lem7  14788  sadass  15031  lubub  16942  lubl  16943  reslmhm2b  18875  ipcl  19797  ma1repveval  20196  mp2pm2mplem5  20434  opnneiss  20732  llyi  21087  nllyi  21088  cfiluweak  21909  cniccibl  23413  ply1term  23764  explog  24144  logrec  24301  4cycl2vnunb  26544  numclwwlkovf2ex  26613  numclwwlk7  26641  lnocoi  26996  hvaddsubass  27282  hvmulcan2  27314  hhssabloilem  27502  hhssnv  27505  homco1  28044  homulass  28045  hoadddir  28047  hoaddsubass  28058  hosubsub4  28061  kbmul  28198  lnopmulsubi  28219  mdsl3  28559  cdj3lem2  28678  probmeasb  29819  signswmnd  29960  bnj563  30067  fnessex  31511  cnicciblnc  32651  incsequz2  32715  ltrncnvatb  34442  jm2.17a  36545  lnrfgtr  36709  ccatw2s1cl  40243  usgredgop  40400  usgr2v1e2w  40478  cusgrsizeinds  40668  4cycl2vnunb-av  41460  frrusgrord0  41503  av-numclwwlkovf2ex  41517  av-numclwwlk7  41545  dignnld  42195
 Copyright terms: Public domain W3C validator