Theorem sbccomieg

Description: Commute two explicit substitutions, using an implicit substitution to rewrite the exiting substitution. (Contributed by Stefan O'Rear, 11-Oct-2014) (Revised by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypothesis	sbccomieg.1	|- ( a = A -> B = C )
Assertion	sbccomieg	|- ( [. A / a ]. [. B / b ]. ph <-> [. C / b ]. [. A / a ]. ph )

Proof

Step	Hyp	Ref	Expression
1		sbccomieg.1	|- ( a = A -> B = C )
2		sbcex	|- ( [. A / a ]. [. B / b ]. ph -> A e. _V )
3		spesbc	|- ( [. C / b ]. [. A / a ]. ph -> E. b [. A / a ]. ph )
4		sbcex	|- ( [. A / a ]. ph -> A e. _V )
5	4	exlimiv	|- ( E. b [. A / a ]. ph -> A e. _V )
6	3 5	syl	|- ( [. C / b ]. [. A / a ]. ph -> A e. _V )
7		nfcv	|- F/_ a C
8		nfsbc1v	|- F/ a [. A / a ]. ph
9	7 8	nfsbcw	|- F/ a [. C / b ]. [. A / a ]. ph
10		sbceq1a	|- ( a = A -> ( ph <-> [. A / a ]. ph ) )
11	1 10	sbceqbid	|- ( a = A -> ( [. B / b ]. ph <-> [. C / b ]. [. A / a ]. ph ) )
12	9 11	sbciegf	|- ( A e. _V -> ( [. A / a ]. [. B / b ]. ph <-> [. C / b ]. [. A / a ]. ph ) )
13	2 6 12	pm5.21nii	|- ( [. A / a ]. [. B / b ]. ph <-> [. C / b ]. [. A / a ]. ph )