Theorem anassrs 62

Description: Associativity for context. (Contributed by Mario Carneiro, 8-Oct-2014.)

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 33	. . . 4 |- R:*
4	2	wctr 34	. . . . 5 |- (S, T):*
5	4	wctl 33	. . . 4 |- S:*
6	3, 5	simpl 22	. . 3 |- (R, S) |= R
7	4	wctr 34	. . 3 |- T:*
8	6, 7	adantr 55	. 2 |- ((R, S), T) |= R
9	3, 5	simpr 23	. . 3 |- (R, S) |= S
10	9, 7	ct1 57	. 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  ax-wctl 31  ax-wctr 32

This theorem is referenced by: (None)