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	⊢ Ⅎ 𝑥 𝐴
	subtr.2	⊢ Ⅎ 𝑥 𝐵
	subtr.3	⊢ Ⅎ 𝑥 𝑌
	subtr.4	⊢ Ⅎ 𝑥 𝑍
	subtr.5	⊢ ( 𝑥 = 𝐴 → 𝑋 = 𝑌 )
	subtr.6	⊢ ( 𝑥 = 𝐵 → 𝑋 = 𝑍 )
Assertion	subtr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 = 𝐵 → 𝑌 = 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		subtr.1	⊢ Ⅎ 𝑥 𝐴
2		subtr.2	⊢ Ⅎ 𝑥 𝐵
3		subtr.3	⊢ Ⅎ 𝑥 𝑌
4		subtr.4	⊢ Ⅎ 𝑥 𝑍
5		subtr.5	⊢ ( 𝑥 = 𝐴 → 𝑋 = 𝑌 )
6		subtr.6	⊢ ( 𝑥 = 𝐵 → 𝑋 = 𝑍 )
7	1 2	nfeq	⊢ Ⅎ 𝑥 𝐴 = 𝐵
8	3 4	nfeq	⊢ Ⅎ 𝑥 𝑌 = 𝑍
9	7 8	nfim	⊢ Ⅎ 𝑥 ( 𝐴 = 𝐵 → 𝑌 = 𝑍 )
10		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝐵 ↔ 𝐴 = 𝐵 ) )
11	5	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( 𝑋 = 𝑍 ↔ 𝑌 = 𝑍 ) )
12	10 11	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = 𝐵 → 𝑋 = 𝑍 ) ↔ ( 𝐴 = 𝐵 → 𝑌 = 𝑍 ) ) )
13	1 9 12 6	vtoclgf	⊢ ( 𝐴 ∈ 𝐶 → ( 𝐴 = 𝐵 → 𝑌 = 𝑍 ) )
14	13	adantr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 = 𝐵 → 𝑌 = 𝑍 ) )