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

Metamath Proof Explorer

Theorem axc16ALT

Description: Alternate proof of axc16 , shorter but requiring ax-10 , ax-11 , ax-13 and using df-nf and df-sb . (Contributed by NM, 17-May-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axc16ALT ⊢ ∀ x x = y → φ → ∀ x φ

Proof

Step Hyp Ref Expression
1 sbequ12 ⊢ x = z → φ ↔ z x φ
2 ax-5 ⊢ φ → ∀ z φ
3 2 hbsb3 ⊢ z x φ → ∀ x z x φ
4 1 3 axc16i ⊢ ∀ x x = y → φ → ∀ x φ