Theorem stoic3 1780

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

Step	Hyp	Ref	Expression
1		stoic3.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		stoic3.2	. . 3 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
3	1, 2	sylan 579	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)
4	3	3impa 1108	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  opelopabt  5438  ordelinel  6349  nelrnfvne  6937  omass  8373  nnmass  8417  f1imaeng  8755  ssfi  8918  domtrfi  8938  genpass  10696  adddir  10897  le2tri3i  11035  addsub12  11164  subdir  11339  ltaddsub  11379  leaddsub  11381  div12  11585  xmulass  12950  fldiv2  13509  modsubdir  13588  digit2  13879  muldivbinom2  13905  ccatass  14221  ccatw2s1cl  14258  repswcshw  14453  s3tpop  14550  absdiflt  14957  absdifle  14958  binomrisefac  15680  cos01gt0  15828  rpnnen2lem4  15854  rpnnen2lem7  15857  sadass  16106  lubub  18144  lubl  18145  symggrplem  18438  reslmhm2b  20231  ipcl  20750  ma1repveval  21628  mp2pm2mplem5  21867  opnneiss  22177  llyi  22533  nllyi  22534  cfiluweak  23355  cniccibl  24910  cnicciblnc  24912  ply1term  25270  explog  25654  logrec  25818  usgredgop  27443  usgr2v1e2w  27522  cusgrsizeinds  27722  clwwlknonex2  28374  4cycl2vnunb  28555  frrusgrord0lem  28604  frrusgrord0  28605  numclwwlk7  28656  lnocoi  29020  hvaddsubass  29304  hvmulcan2  29336  hhssabloilem  29524  hhssnv  29527  homco1  30064  homulass  30065  hoadddir  30067  hoaddsubass  30078  hosubsub4  30081  kbmul  30218  lnopmulsubi  30239  mdsl3  30579  cdj3lem2  30698  probmeasb  32297  signswmnd  32436  bnj563  32623  revpfxsfxrev  32977  lfuhgr2  32980  fnessex  34462  incsequz2  35834  ltrncnvatb  38079  jm2.17a  40698  lnrfgtr  40861  prsssprel  44828  dignnld  45837