Theorem anasss 61

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

Hypothesis

Ref	Expression
an32s.1	|- ((R, S), T) |= A

Assertion

Ref	Expression
anasss	|- (R, (S, T)) |= A

Proof of Theorem anasss

Step	Hyp	Ref	Expression
1		an32s.1	. . . . . . . 8 |- ((R, S), T) |= A
2	1	ax-cb1 29	. . . . . . 7 |- ((R, S), T):*
3	2	wctl 33	. . . . . 6 |- (R, S):*
4	3	id 25	. . . . 5 |- (R, S) |= (R, S)
5	4	ancoms 54	. . . 4 |- (S, R) |= (R, S)
6	5, 1	sylan 59	. . 3 |- ((S, R), T) |= A
7	6	an32s 60	. 2 |- ((S, T), R) |= A
8	7	ancoms 54	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-id 24  ax-cb1 29  ax-wctl 31  ax-wctr 32

This theorem is referenced by: (None)