Theorem stoic3 1809

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 592	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)
4	3	3impa 1127	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  opelopabt  5510  ordelinel  6461  nelrnfvne  7070  omass  8567  nnmass  8612  f1imaeng  9020  ssfi  9167  genpass  11018  adddir  11221  le2tri3i  11364  addsub12  11494  subdir  11672  ltaddsub  11712  leaddsub  11714  div12  11918  xmulass  13339  fldiv2  13922  modsubdir  14004  digit2  14300  muldivbinom2  14327  ccatass  14654  ccatw2s1cl  14692  revpfxsfxrev  14837  repswcshw  14883  s3tpop  14980  absdiflt  15405  absdifle  15406  binomrisefac  16128  cos01gt0  16279  rpnnen2lem4  16305  rpnnen2lem7  16308  sadass  16561  lubub  18599  lubl  18600  symggrplem  18993  reslmhm2b  21238  cncrng  21606  ipcl  21846  ma1repveval  22793  mp2pm2mplem5  23035  opnneiss  23343  llyi  23700  nllyi  23701  cfiluweak  24520  cniccibl  26068  cnicciblnc  26070  ply1term  26429  explog  26831  logrec  27000  lfuhgr2  29606  usgredgop  29630  usgr2v1e2w  29712  cusgrsizeinds  29912  clwwlknonex2  30579  4cycl2vnunb  30770  frrusgrord0lem  30819  frrusgrord0  30820  numclwwlk7  30871  lnocoi  31238  hvaddsubass  31522  hvmulcan2  31554  hhssabloilem  31742  hhssnv  31745  homco1  32282  homulass  32283  hoadddir  32285  hoaddsubass  32296  hosubsub4  32299  kbmul  32436  lnopmulsubi  32457  mdsl3  32797  cdj3lem2  32916  probmeasb  34941  signswmnd  35065  bnj563  35253  fineqvnttrclselem2  35648  fineqvnttrclselem3  35649  karddom  35687  kardsdom  35688  kardexen  35689  nmulle  36797  fnessex  36965  incsequz2  38499  ltrncnvatb  41011  jm2.17a  43801  lnrfgtr  43961  bdaybndex  44271  limsupvaluz2  46566  prsssprel  48388  dignnld  49533