Theorem axc16i

Description: Inference with axc16 as its conclusion. Usage of axc16 is preferred since it requires fewer axioms. (Contributed by NM, 20-May-2008) (Proof modification is discouraged.) (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	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 𝜑 ) )