Metamath Proof Explorer

Theorem ax12indi

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Implication case. (Contributed by NM, 21-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	ax12indn.1	$⊢ \neg \forall x x = y \to (x = y \to (φ \to \forall x (x = y \to φ)))$
		ax12indi.2	$⊢ \neg \forall x x = y \to (x = y \to (ψ \to \forall x (x = y \to ψ)))$
	Assertion	ax12indi	$⊢ \neg \forall x x = y \to (x = y \to ((φ \to ψ) \to \forall x (x = y \to (φ \to ψ))))$

Proof

Step	Hyp	Ref	Expression
1		ax12indn.1	$⊢ \neg \forall x x = y \to (x = y \to (φ \to \forall x (x = y \to φ)))$
2		ax12indi.2	$⊢ \neg \forall x x = y \to (x = y \to (ψ \to \forall x (x = y \to ψ)))$
3	1	ax12indn	$⊢ \neg \forall x x = y \to (x = y \to (\neg φ \to \forall x (x = y \to \neg φ)))$
4	3	imp	$⊢ (\neg \forall x x = y \land x = y) \to (\neg φ \to \forall x (x = y \to \neg φ))$
5		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
6	5	imim2i	$⊢ (x = y \to \neg φ) \to (x = y \to (φ \to ψ))$
7	6	alimi	$⊢ \forall x (x = y \to \neg φ) \to \forall x (x = y \to (φ \to ψ))$
8	4 7	syl6	$⊢ (\neg \forall x x = y \land x = y) \to (\neg φ \to \forall x (x = y \to (φ \to ψ)))$
9	2	imp	$⊢ (\neg \forall x x = y \land x = y) \to (ψ \to \forall x (x = y \to ψ))$
10		ax-1	$⊢ ψ \to (φ \to ψ)$
11	10	imim2i	$⊢ (x = y \to ψ) \to (x = y \to (φ \to ψ))$
12	11	alimi	$⊢ \forall x (x = y \to ψ) \to \forall x (x = y \to (φ \to ψ))$
13	9 12	syl6	$⊢ (\neg \forall x x = y \land x = y) \to (ψ \to \forall x (x = y \to (φ \to ψ)))$
14	8 13	jad	$⊢ (\neg \forall x x = y \land x = y) \to ((φ \to ψ) \to \forall x (x = y \to (φ \to ψ)))$
15	14	ex	$⊢ \neg \forall x x = y \to (x = y \to ((φ \to ψ) \to \forall x (x = y \to (φ \to ψ))))$