Metamath Proof Explorer

Theorem hbimtg

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

Ref Expression
Assertion hbimtg ⊢ ∀ x φ → ∀ x χ ∧ ψ → ∀ x θ → χ → ψ → ∀ x φ → θ

Proof

Step Hyp Ref Expression
1 hbntg ⊢ ∀ x φ → ∀ x χ → ¬ χ → ∀ x ¬ φ
2 pm2.21 ⊢ ¬ φ → φ → θ
3 2 alimi ⊢ ∀ x ¬ φ → ∀ x φ → θ
4 1 3 syl6 ⊢ ∀ x φ → ∀ x χ → ¬ χ → ∀ x φ → θ
5 4 adantr ⊢ ∀ x φ → ∀ x χ ∧ ψ → ∀ x θ → ¬ χ → ∀ x φ → θ
6 ala1 ⊢ ∀ x θ → ∀ x φ → θ
7 6 imim2i ⊢ ψ → ∀ x θ → ψ → ∀ x φ → θ
8 7 adantl ⊢ ∀ x φ → ∀ x χ ∧ ψ → ∀ x θ → ψ → ∀ x φ → θ
9 5 8 jad ⊢ ∀ x φ → ∀ x χ ∧ ψ → ∀ x θ → χ → ψ → ∀ x φ → θ