Theorem hbimtg

Description: A more general and closed form of hbim . (Contributed by Scott Fenton, 13-Dec-2010)

	Ref	Expression
Assertion	hbimtg	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) ∧ ( 𝜓 → ∀ 𝑥 𝜃 ) ) → ( ( 𝜒 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hbntg	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) → ( ¬ 𝜒 → ∀ 𝑥 ¬ 𝜑 ) )
2		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜃 ) )
3	2	alimi	⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ( 𝜑 → 𝜃 ) )
4	1 3	syl6	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) → ( ¬ 𝜒 → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )
5	4	adantr	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) ∧ ( 𝜓 → ∀ 𝑥 𝜃 ) ) → ( ¬ 𝜒 → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )
6		ala1	⊢ ( ∀ 𝑥 𝜃 → ∀ 𝑥 ( 𝜑 → 𝜃 ) )
7	6	imim2i	⊢ ( ( 𝜓 → ∀ 𝑥 𝜃 ) → ( 𝜓 → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )
8	7	adantl	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) ∧ ( 𝜓 → ∀ 𝑥 𝜃 ) ) → ( 𝜓 → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )
9	5 8	jad	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) ∧ ( 𝜓 → ∀ 𝑥 𝜃 ) ) → ( ( 𝜒 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )