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

Metamath Proof Explorer

Theorem axc16gb

Description: Biconditional strengthening of axc16g . (Contributed by NM, 15-May-1993)

Ref Expression
Assertion axc16gb ⊢ ∀ x x = y → φ ↔ ∀ z φ

Proof

Step Hyp Ref Expression
1 axc16g ⊢ ∀ x x = y → φ → ∀ z φ
2 sp ⊢ ∀ z φ → φ
3 1 2 impbid1 ⊢ ∀ x x = y → φ ↔ ∀ z φ