Theorem anassrs 57

Description: Associativity for context.

Hypothesis

Ref	Expression
anassrs.1	⊢ (R, (S, T))⊧A

Assertion

Ref	Expression
anassrs	⊢ ((R, S), T)⊧A

Proof of Theorem anassrs

Step	Hyp	Ref	Expression
1		anassrs.1	. . . . . 6 ⊢ (R, (S, T))⊧A
2	1	ax-cb1 29	. . . . 5 ⊢ (R, (S, T)):∗
3	2	wctl 31	. . . 4 ⊢ R:∗
4	2	wctr 32	. . . . 5 ⊢ (S, T):∗
5	4	wctl 31	. . . 4 ⊢ S:∗
6	3, 5	simpl 22	. . 3 ⊢ (R, S)⊧R
7	4	wctr 32	. . 3 ⊢ T:∗
8	6, 7	adantr 50	. 2 ⊢ ((R, S), T)⊧R
9	3, 5	simpr 23	. . 3 ⊢ (R, S)⊧S
10	9, 7	ct1 52	. 2 ⊢ ((R, S), T)⊧(S, T)
11	8, 10, 1	syl2anc 19	1 ⊢ ((R, S), T)⊧A

Syntax hints:  kct 10  ⊧wffMMJ2 11

This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-cb1 29

This theorem is referenced by: (None)