Theorem subtr

Description: Transitivity of implicit substitution. (Contributed by Jeff Hankins, 13-Sep-2009) (Proof shortened by Mario Carneiro, 11-Dec-2016)

	Ref	Expression
Hypotheses	subtr.1	|- F/_ x A
	subtr.2	|- F/_ x B
	subtr.3	|- F/_ x Y
	subtr.4	|- F/_ x Z
	subtr.5	|- ( x = A -> X = Y )
	subtr.6	|- ( x = B -> X = Z )
Assertion	subtr	|- ( ( A e. C /\ B e. D ) -> ( A = B -> Y = Z ) )

Proof

Step	Hyp	Ref	Expression
1		subtr.1	|- F/_ x A
2		subtr.2	|- F/_ x B
3		subtr.3	|- F/_ x Y
4		subtr.4	|- F/_ x Z
5		subtr.5	|- ( x = A -> X = Y )
6		subtr.6	|- ( x = B -> X = Z )
7	1 2	nfeq	|- F/ x A = B
8	3 4	nfeq	|- F/ x Y = Z
9	7 8	nfim	|- F/ x ( A = B -> Y = Z )
10		eqeq1	|- ( x = A -> ( x = B <-> A = B ) )
11	5	eqeq1d	|- ( x = A -> ( X = Z <-> Y = Z ) )
12	10 11	imbi12d	|- ( x = A -> ( ( x = B -> X = Z ) <-> ( A = B -> Y = Z ) ) )
13	1 9 12 6	vtoclgf	|- ( A e. C -> ( A = B -> Y = Z ) )
14	13	adantr	|- ( ( A e. C /\ B e. D ) -> ( A = B -> Y = Z ) )