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

Metamath Proof Explorer

Theorem axc16i

Description: Inference with axc16 as its conclusion. (Contributed by NM, 20-May-2008) (Proof modification is discouraged.) Usage of this theorem is discouraged because it depends on ax-13 . Use axc16 instead. (New usage is discouraged.)

Ref Expression
Hypotheses axc16i.1 ⊢ x = z → φ ↔ ψ
axc16i.2 ⊢ ψ → ∀ x ψ
Assertion axc16i ⊢ ∀ x x = y → φ → ∀ x φ

Proof

Step Hyp Ref Expression
1 axc16i.1 ⊢ x = z → φ ↔ ψ
2 axc16i.2 ⊢ ψ → ∀ x ψ
3 nfv ⊢ Ⅎ z x = y
4 nfv ⊢ Ⅎ x z = y
5 ax7 ⊢ x = z → x = y → z = y
6 3 4 5 cbv3 ⊢ ∀ x x = y → ∀ z z = y
7 ax7 ⊢ z = x → z = y → x = y
8 7 spimvw ⊢ ∀ z z = y → x = y
9 equcomi ⊢ x = y → y = x
10 equcomi ⊢ z = y → y = z
11 ax7 ⊢ y = z → y = x → z = x
12 10 11 syl ⊢ z = y → y = x → z = x
13 9 12 syl5com ⊢ x = y → z = y → z = x
14 13 alimdv ⊢ x = y → ∀ z z = y → ∀ z z = x
15 8 14 mpcom ⊢ ∀ z z = y → ∀ z z = x
16 equcomi ⊢ z = x → x = z
17 16 alimi ⊢ ∀ z z = x → ∀ z x = z
18 15 17 syl ⊢ ∀ z z = y → ∀ z x = z
19 1 biimpcd ⊢ φ → x = z → ψ
20 19 alimdv ⊢ φ → ∀ z x = z → ∀ z ψ
21 2 nf5i ⊢ Ⅎ x ψ
22 nfv ⊢ Ⅎ z φ
23 1 biimprd ⊢ x = z → ψ → φ
24 16 23 syl ⊢ z = x → ψ → φ
25 21 22 24 cbv3 ⊢ ∀ z ψ → ∀ x φ
26 20 25 syl6com ⊢ ∀ z x = z → φ → ∀ x φ
27 6 18 26 3syl ⊢ ∀ x x = y → φ → ∀ x φ