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

Metamath Proof Explorer

Theorem ax12i

Description: Inference that has ax-12 (without A. y ) as its conclusion. Uses only Tarski's FOL axiom schemes. The hypotheses may be eliminable without using ax-12 in special cases. Proof similar to Lemma 16 of Tarski p. 70. (Contributed by NM, 20-May-2008)

	Ref	Expression
Hypotheses	ax12i.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	ax12i.2	$⊢ ψ \to \forall x ψ$
Assertion	ax12i	$⊢ x = y \to (φ \to \forall x (x = y \to φ))$

Proof

Step	Hyp	Ref	Expression
1		ax12i.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		ax12i.2	$⊢ ψ \to \forall x ψ$
3	1	biimprcd	$⊢ ψ \to (x = y \to φ)$
4	2 3	alrimih	$⊢ ψ \to \forall x (x = y \to φ)$
5	1 4	biimtrdi	$⊢ x = y \to (φ \to \forall x (x = y \to φ))$