This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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