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

This proof depends on syntax axioms:  kct 10  ⊧wffMMJ2 11

This proof depends on 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 used by: (None)