Metamath Proof Explorer

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 ⊢ Ⅎ _ x A
subtr.2 ⊢ Ⅎ _ x B
subtr2.3 ⊢ Ⅎ x ψ
subtr2.4 ⊢ Ⅎ x χ
subtr2.5 ⊢ x = A → φ ↔ ψ
subtr2.6 ⊢ x = B → φ ↔ χ
Assertion subtr2 ⊢ A ∈ C ∧ B ∈ D → A = B → ψ ↔ χ

Proof

Step Hyp Ref Expression
1 subtr.1 ⊢ Ⅎ _ x A
2 subtr.2 ⊢ Ⅎ _ x B
3 subtr2.3 ⊢ Ⅎ x ψ
4 subtr2.4 ⊢ Ⅎ x χ
5 subtr2.5 ⊢ x = A → φ ↔ ψ
6 subtr2.6 ⊢ x = B → φ ↔ χ
7 1 2 nfeq ⊢ Ⅎ x A = B
8 3 4 nfbi ⊢ Ⅎ x ψ ↔ χ
9 7 8 nfim ⊢ Ⅎ x A = B → ψ ↔ χ
10 eqeq1 ⊢ x = A → x = B ↔ A = B
11 5 bibi1d ⊢ x = A → φ ↔ χ ↔ ψ ↔ χ
12 10 11 imbi12d ⊢ x = A → x = B → φ ↔ χ ↔ A = B → ψ ↔ χ
13 1 9 12 6 vtoclgf ⊢ A ∈ C → A = B → ψ ↔ χ
14 13 adantr ⊢ A ∈ C ∧ B ∈ D → A = B → ψ ↔ χ