Metamath Proof Explorer

Theorem ichbidv

Description: Formula building rule for interchangeability (deduction). (Contributed by SN, 4-May-2024)

Ref Expression
Hypothesis ichbidv.1 ⊢ φ → ψ ↔ χ
Assertion ichbidv ⊢ φ → x ⇄ y ψ ↔ x ⇄ y χ

Proof

Step Hyp Ref Expression
1 ichbidv.1 ⊢ φ → ψ ↔ χ
2 1 sbbidv ⊢ φ → a y ψ ↔ a y χ
3 2 sbbidv ⊢ φ → y x a y ψ ↔ y x a y χ
4 3 sbbidv ⊢ φ → x a y x a y ψ ↔ x a y x a y χ
5 4 1 bibi12d ⊢ φ → x a y x a y ψ ↔ ψ ↔ x a y x a y χ ↔ χ
6 5 albidv ⊢ φ → ∀ y x a y x a y ψ ↔ ψ ↔ ∀ y x a y x a y χ ↔ χ
7 6 albidv ⊢ φ → ∀ x ∀ y x a y x a y ψ ↔ ψ ↔ ∀ x ∀ y x a y x a y χ ↔ χ
8 df-ich ⊢ x ⇄ y ψ ↔ ∀ x ∀ y x a y x a y ψ ↔ ψ
9 df-ich ⊢ x ⇄ y χ ↔ ∀ x ∀ y x a y x a y χ ↔ χ
10 7 8 9 3bitr4g ⊢ φ → x ⇄ y ψ ↔ x ⇄ y χ