Theorem hbimg

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

	Ref	Expression
Hypotheses	hbg.1	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
	hbg.2	⊢ ( 𝜒 → ∀ 𝑥 𝜃 )
Assertion	hbimg	⊢ ( ( 𝜓 → 𝜒 ) → ∀ 𝑥 ( 𝜑 → 𝜃 ) )

Proof

Step	Hyp	Ref	Expression
1		hbg.1	⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
2		hbg.2	⊢ ( 𝜒 → ∀ 𝑥 𝜃 )
3	1	ax-gen	⊢ ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜓 )
4		hbimtg	⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜓 ) ∧ ( 𝜒 → ∀ 𝑥 𝜃 ) ) → ( ( 𝜓 → 𝜒 ) → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )
5	3 2 4	mp2an	⊢ ( ( 𝜓 → 𝜒 ) → ∀ 𝑥 ( 𝜑 → 𝜃 ) )