Theorem subtr2

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

	Ref	Expression
Hypotheses	subtr.1	⊢ Ⅎ 𝑥 𝐴
	subtr.2	⊢ Ⅎ 𝑥 𝐵
	subtr2.3	⊢ Ⅎ 𝑥 𝜓
	subtr2.4	⊢ Ⅎ 𝑥 𝜒
	subtr2.5	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	subtr2.6	⊢ ( 𝑥 = 𝐵 → ( 𝜑 ↔ 𝜒 ) )
Assertion	subtr2	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) )

Proof

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