Metamath Proof Explorer

Theorem hbimpg

Description: A closed form of hbim . Derived from hbimpgVD . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion hbimpg ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → ∀ x φ → ψ → ∀ x φ → ψ

Proof

Step Hyp Ref Expression
1 hba1 ⊢ ∀ x φ → ∀ x φ → ∀ x ∀ x φ → ∀ x φ
2 hba1 ⊢ ∀ x ψ → ∀ x ψ → ∀ x ∀ x ψ → ∀ x ψ
3 1 2 hban ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → ∀ x ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ
4 hbntal ⊢ ∀ x φ → ∀ x φ → ∀ x ¬ φ → ∀ x ¬ φ
5 4 adantr ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → ∀ x ¬ φ → ∀ x ¬ φ
6 5 19.21bi ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → ¬ φ → ∀ x ¬ φ
7 pm2.21 ⊢ ¬ φ → φ → ψ
8 7 alimi ⊢ ∀ x ¬ φ → ∀ x φ → ψ
9 6 8 syl6 ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → ¬ φ → ∀ x φ → ψ
10 simpr ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → ∀ x ψ → ∀ x ψ
11 10 19.21bi ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → ψ → ∀ x ψ
12 ax-1 ⊢ ψ → φ → ψ
13 12 alimi ⊢ ∀ x ψ → ∀ x φ → ψ
14 11 13 syl6 ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → ψ → ∀ x φ → ψ
15 9 14 jad ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → φ → ψ → ∀ x φ → ψ
16 3 15 alrimih ⊢ ∀ x φ → ∀ x φ ∧ ∀ x ψ → ∀ x ψ → ∀ x φ → ψ → ∀ x φ → ψ