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	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ∀ 𝑥 ( ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hba1	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) )
2		hba1	⊢ ( ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) → ∀ 𝑥 ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) )
3	1 2	hban	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) )
4		hbntal	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) → ∀ 𝑥 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
5	4	adantr	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ∀ 𝑥 ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
6	5	19.21bi	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ( ¬ 𝜑 → ∀ 𝑥 ¬ 𝜑 ) )
7		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
8	7	alimi	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ( 𝜑 → 𝜓 ) )
9	6 8	syl6	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ( ¬ 𝜑 → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
10		simpr	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) )
11	10	19.21bi	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ( 𝜓 → ∀ 𝑥 𝜓 ) )
12		ax-1	⊢ ( 𝜓 → ( 𝜑 → 𝜓 ) )
13	12	alimi	⊢ ( ∀ 𝑥 𝜓 → ∀ 𝑥 ( 𝜑 → 𝜓 ) )
14	11 13	syl6	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ( 𝜓 → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
15	9 14	jad	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ( ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )
16	3 15	alrimih	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜑 ) ∧ ∀ 𝑥 ( 𝜓 → ∀ 𝑥 𝜓 ) ) → ∀ 𝑥 ( ( 𝜑 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜓 ) ) )