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

Metamath Proof Explorer

Theorem 19.16

Description: Theorem 19.16 of Margaris p. 90. (Contributed by NM, 12-Mar-1993)

Ref Expression
Hypothesis 19.16.1 ⊢ Ⅎ x φ
Assertion 19.16 ⊢ ∀ x φ ↔ ψ → φ ↔ ∀ x ψ

Proof

Step Hyp Ref Expression
1 19.16.1 ⊢ Ⅎ x φ
2 1 19.3 ⊢ ∀ x φ ↔ φ
3 albi ⊢ ∀ x φ ↔ ψ → ∀ x φ ↔ ∀ x ψ
4 2 3 bitr3id ⊢ ∀ x φ ↔ ψ → φ ↔ ∀ x ψ