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 ⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜓 ) )
axc16i.2 ⊢ ( 𝜓 → ∀ 𝑥 𝜓 )
Assertion axc16i ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 𝜑 ) )

Proof

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