Theorem an32s 60

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

Hypothesis

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

Assertion

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

Proof of Theorem an32s

Step	Hyp	Ref	Expression
1		an32s.1	. . . . . . 7 ⊢ ((R, S), T)⊧A
2	1	ax-cb1 29	. . . . . 6 ⊢ ((R, S), T):∗
3	2	wctl 33	. . . . 5 ⊢ (R, S):∗
4	3	wctl 33	. . . 4 ⊢ R:∗
5	2	wctr 34	. . . 4 ⊢ T:∗
6	4, 5	simpl 22	. . 3 ⊢ (R, T)⊧R
7	3	wctr 34	. . 3 ⊢ S:∗
8	6, 7	ct1 57	. 2 ⊢ ((R, T), S)⊧(R, S)
9	4, 5	simpr 23	. . 3 ⊢ (R, T)⊧T
10	9, 7	adantr 55	. 2 ⊢ ((R, T), S)⊧T
11	8, 10, 1	syl2anc 19	1 ⊢ ((R, T), S)⊧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:  anasss  61  con2d  161  ax3  205