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 ⊢ φ → ∀ x ψ
hbg.2 ⊢ χ → ∀ x θ
Assertion hbimg ⊢ ψ → χ → ∀ x φ → θ

Proof

Step Hyp Ref Expression
1 hbg.1 ⊢ φ → ∀ x ψ
2 hbg.2 ⊢ χ → ∀ x θ
3 1 ax-gen ⊢ ∀ x φ → ∀ x ψ
4 hbimtg ⊢ ∀ x φ → ∀ x ψ ∧ χ → ∀ x θ → ψ → χ → ∀ x φ → θ
5 3 2 4 mp2an ⊢ ψ → χ → ∀ x φ → θ