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

Theorem stoic3 1691
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 486 . 2 (((𝜑𝜓) ∧ 𝜃) → 𝜏)
433impa 1250 1 ((𝜑𝜓𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  opelopabt  4899  ordelinel  5725  ordelinelOLD  5726  nelrnfvne  6243  omass  7521  nnmass  7565  f1imaeng  7876  genpass  9684  adddir  9884  le2tri3i  10015  addsub12  10142  subdir  10312  ltaddsub  10348  leaddsub  10350  div12  10553  xmulass  11943  fldiv2  12474  modsubdir  12553  digit2  12811  muldivbinom2  12861  ccatass  13167  ccatw2s1len  13197  repswcshw  13352  s3tpop  13447  absdiflt  13848  absdifle  13849  binomrisefac  14555  cos01gt0  14703  rpnnen2lem4  14728  rpnnen2lem7  14731  sadass  14974  lubub  16885  lubl  16886  reslmhm2b  18818  ipcl  19739  ma1repveval  20135  mp2pm2mplem5  20373  opnneiss  20671  llyi  21026  nllyi  21027  cfiluweak  21848  cniccibl  23327  ply1term  23678  explog  24058  logrec  24215  4cycl2vnunb  26307  numclwwlkovf2ex  26376  numclwwlk7  26404  lnocoi  26799  hvaddsubass  27085  hvmulcan2  27117  hhssabloilem  27305  hhssnv  27308  homco1  27847  homulass  27848  hoadddir  27850  hoaddsubass  27861  hosubsub4  27864  kbmul  28001  lnopmulsubi  28022  mdsl3  28362  cdj3lem2  28481  probmeasb  29622  signswmnd  29763  bnj563  29870  fnessex  31314  cnicciblnc  32451  incsequz2  32515  ltrncnvatb  34242  jm2.17a  36345  lnrfgtr  36509  ccatw2s1cl  40045  usgredgop  40399  usgr2v1e2w  40477  cusgrsizeinds  40667  4cycl2vnunb-av  41459  frrusgrord0  41502  av-numclwwlkovf2ex  41516  av-numclwwlk7  41544  dignnld  42194
  Copyright terms: Public domain W3C validator