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

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

Proof

Step Hyp Ref Expression
1 hbntg ⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) → ( ¬ 𝜒 → ∀ 𝑥 ¬ 𝜑 ) )
2 pm2.21 ⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜃 ) )
3 2 alimi ⊢ ( ∀ 𝑥 ¬ 𝜑 → ∀ 𝑥 ( 𝜑 → 𝜃 ) )
4 1 3 syl6 ⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) → ( ¬ 𝜒 → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )
5 4 adantr ⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) ∧ ( 𝜓 → ∀ 𝑥 𝜃 ) ) → ( ¬ 𝜒 → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )
6 ala1 ⊢ ( ∀ 𝑥 𝜃 → ∀ 𝑥 ( 𝜑 → 𝜃 ) )
7 6 imim2i ⊢ ( ( 𝜓 → ∀ 𝑥 𝜃 ) → ( 𝜓 → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )
8 7 adantl ⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) ∧ ( 𝜓 → ∀ 𝑥 𝜃 ) ) → ( 𝜓 → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )
9 5 8 jad ⊢ ( ( ∀ 𝑥 ( 𝜑 → ∀ 𝑥 𝜒 ) ∧ ( 𝜓 → ∀ 𝑥 𝜃 ) ) → ( ( 𝜒 → 𝜓 ) → ∀ 𝑥 ( 𝜑 → 𝜃 ) ) )