This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem albi

Description: Theorem 19.15 of Margaris p. 90. (Contributed by NM, 24-Jan-1993)

Ref Expression
Assertion albi ⊢ ∀ x φ ↔ ψ → ∀ x φ ↔ ∀ x ψ

Proof

Step Hyp Ref Expression
1 biimp ⊢ φ ↔ ψ → φ → ψ
2 1 al2imi ⊢ ∀ x φ ↔ ψ → ∀ x φ → ∀ x ψ
3 biimpr ⊢ φ ↔ ψ → ψ → φ
4 3 al2imi ⊢ ∀ x φ ↔ ψ → ∀ x ψ → ∀ x φ
5 2 4 impbid ⊢ ∀ x φ ↔ ψ → ∀ x φ ↔ ∀ x ψ