Theorem stoic3 1701

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	|- ( ( ph /\ ps ) -> ch )
stoic3.2	|- ( ( ch /\ th ) -> ta )

Assertion

Ref	Expression
stoic3	|- ( ( ph /\ ps /\ th ) -> ta )

Proof of Theorem stoic3

Step	Hyp	Ref	Expression
1		stoic3.1	. . 3 |- ( ( ph /\ ps ) -> ch )
2		stoic3.2	. . 3 |- ( ( ch /\ th ) -> ta )
3	1, 2	sylan 488	. 2 |- ( ( ( ph /\ ps ) /\ th ) -> ta )
4	3	3impa 1259	1 |- ( ( ph /\ ps /\ th ) -> ta )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  opelopabt  4987  ordelinel  5825  ordelinelOLD  5826  nelrnfvne  6353  omass  7660  nnmass  7704  f1imaeng  8016  genpass  9831  adddir  10031  le2tri3i  10167  addsub12  10294  subdir  10464  ltaddsub  10502  leaddsub  10504  div12  10707  xmulass  12117  fldiv2  12660  modsubdir  12739  digit2  12997  muldivbinom2  13047  ccatass  13371  ccatw2s1cl  13401  ccatw2s1len  13402  repswcshw  13558  s3tpop  13654  absdiflt  14057  absdifle  14058  binomrisefac  14773  cos01gt0  14921  rpnnen2lem4  14946  rpnnen2lem7  14949  sadass  15193  lubub  17119  lubl  17120  reslmhm2b  19054  ipcl  19978  ma1repveval  20377  mp2pm2mplem5  20615  opnneiss  20922  llyi  21277  nllyi  21278  cfiluweak  22099  cniccibl  23607  ply1term  23960  explog  24340  logrec  24501  usgredgop  26065  usgr2v1e2w  26144  cusgrsizeinds  26348  4cycl2vnunb  27154  frrusgrord0lem  27203  frrusgrord0  27204  numclwwlkovf2ex  27219  numclwwlk7  27249  lnocoi  27612  hvaddsubass  27898  hvmulcan2  27930  hhssabloilem  28118  hhssnv  28121  homco1  28660  homulass  28661  hoadddir  28663  hoaddsubass  28674  hosubsub4  28677  kbmul  28814  lnopmulsubi  28835  mdsl3  29175  cdj3lem2  29294  probmeasb  30492  signswmnd  30634  bnj563  30813  fnessex  32341  cnicciblnc  33481  incsequz2  33545  ltrncnvatb  35424  jm2.17a  37527  lnrfgtr  37690  prsssprel  41738  dignnld  42397