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\phi$$
	nfim1.2	$$⊢\phi \to Ⅎx\psi$$
Assertion	nfim1	$$⊢Ⅎx\left(\phi \to \psi \right)$$

Proof

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