Theorem hbimpg

Description: A closed form of hbim . Derived from hbimpgVD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hbimpg	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \forall x\left(\left(\phi \to \psi \right)\to \forall x\left(\phi \to \psi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hba1	$$⊢\forall x\left(\phi \to \forall x\phi \right)\to \forall x\forall x\left(\phi \to \forall x\phi \right)$$
2		hba1	$$⊢\forall x\left(\psi \to \forall x\psi \right)\to \forall x\forall x\left(\psi \to \forall x\psi \right)$$
3	1 2	hban	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \forall x\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)$$
4		hbntal	$$⊢\forall x\left(\phi \to \forall x\phi \right)\to \forall x\left(\neg \phi \to \forall x\neg \phi \right)$$
5	4	adantr	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \forall x\left(\neg \phi \to \forall x\neg \phi \right)$$
6	5	19.21bi	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \left(\neg \phi \to \forall x\neg \phi \right)$$
7		pm2.21	$$⊢\neg \phi \to \left(\phi \to \psi \right)$$
8	7	alimi	$$⊢\forall x\neg \phi \to \forall x\left(\phi \to \psi \right)$$
9	6 8	syl6	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \left(\neg \phi \to \forall x\left(\phi \to \psi \right)\right)$$
10		simpr	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \forall x\left(\psi \to \forall x\psi \right)$$
11	10	19.21bi	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \left(\psi \to \forall x\psi \right)$$
12		ax-1	$$⊢\psi \to \left(\phi \to \psi \right)$$
13	12	alimi	$$⊢\forall x\psi \to \forall x\left(\phi \to \psi \right)$$
14	11 13	syl6	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \left(\psi \to \forall x\left(\phi \to \psi \right)\right)$$
15	9 14	jad	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \left(\left(\phi \to \psi \right)\to \forall x\left(\phi \to \psi \right)\right)$$
16	3 15	alrimih	$$⊢\left(\forall x\left(\phi \to \forall x\phi \right)\wedge \forall x\left(\psi \to \forall x\psi \right)\right)\to \forall x\left(\left(\phi \to \psi \right)\to \forall x\left(\phi \to \psi \right)\right)$$