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

Theorem stoic3 1778
 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
StepHypRef Expression
1 stoic3.1 . . 3 ((𝜑𝜓) → 𝜒)
2 stoic3.2 . . 3 ((𝜒𝜃) → 𝜏)
31, 2sylan 583 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜏)
433impa 1107 1 ((𝜑𝜓𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  opelopabt  5407  ordelinel  6277  nelrnfvne  6834  omass  8198  nnmass  8242  f1imaeng  8561  genpass  10425  adddir  10626  le2tri3i  10764  addsub12  10893  subdir  11068  ltaddsub  11108  leaddsub  11110  div12  11314  xmulass  12675  fldiv2  13231  modsubdir  13310  digit2  13600  muldivbinom2  13626  ccatass  13940  ccatw2s1cl  13977  repswcshw  14172  s3tpop  14269  absdiflt  14675  absdifle  14676  binomrisefac  15394  cos01gt0  15542  rpnnen2lem4  15568  rpnnen2lem7  15571  sadass  15816  lubub  17727  lubl  17728  symggrplem  18047  reslmhm2b  19821  ipcl  20772  ma1repveval  21175  mp2pm2mplem5  21413  opnneiss  21721  llyi  22077  nllyi  22078  cfiluweak  22899  cniccibl  24442  cnicciblnc  24444  ply1term  24799  explog  25183  logrec  25347  usgredgop  26961  usgr2v1e2w  27040  cusgrsizeinds  27240  clwwlknonex2  27892  4cycl2vnunb  28073  frrusgrord0lem  28122  frrusgrord0  28123  numclwwlk7  28174  lnocoi  28538  hvaddsubass  28822  hvmulcan2  28854  hhssabloilem  29042  hhssnv  29045  homco1  29582  homulass  29583  hoadddir  29585  hoaddsubass  29596  hosubsub4  29599  kbmul  29736  lnopmulsubi  29757  mdsl3  30097  cdj3lem2  30216  probmeasb  31715  signswmnd  31854  bnj563  32041  revpfxsfxrev  32389  lfuhgr2  32392  fnessex  33721  incsequz2  35099  ltrncnvatb  37346  jm2.17a  39757  lnrfgtr  39920  prsssprel  43871  dignnld  44882
 Copyright terms: Public domain W3C validator