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

Metamath Proof Explorer

Theorem nfim1

Description: A closed form of nfim . (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 2-Jan-2018) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021)

		Ref	Expression
	Hypotheses	nfim1.1	$⊢ Ⅎ x φ$
		nfim1.2	$⊢ φ \to Ⅎ x ψ$
	Assertion	nfim1	$⊢ Ⅎ x (φ \to ψ)$

Proof

Step	Hyp	Ref	Expression
1		nfim1.1	$⊢ Ⅎ x φ$
2		nfim1.2	$⊢ φ \to Ⅎ x ψ$
3		nf3	$⊢ Ⅎ x φ \leftrightarrow (\forall x φ \lor \forall x \neg φ)$
4	1 3	mpbi	$⊢ (\forall x φ \lor \forall x \neg φ)$
5		nftht	$⊢ \forall x φ \to Ⅎ x φ$
6	2	sps	$⊢ \forall x φ \to Ⅎ x ψ$
7	5 6	nfimd	$⊢ \forall x φ \to Ⅎ x (φ \to ψ)$
8		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
9	8	alimi	$⊢ \forall x \neg φ \to \forall x (φ \to ψ)$
10		nftht	$⊢ \forall x (φ \to ψ) \to Ⅎ x (φ \to ψ)$
11	9 10	syl	$⊢ \forall x \neg φ \to Ⅎ x (φ \to ψ)$
12	7 11	jaoi	$⊢ (\forall x φ \lor \forall x \neg φ) \to Ⅎ x (φ \to ψ)$
13	4 12	ax-mp	$⊢ Ⅎ x (φ \to ψ)$