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

Metamath Proof Explorer

Theorem alrimdd

Description: Deduction form of Theorem 19.21 of Margaris p. 90, see 19.21 . (Contributed by Mario Carneiro, 24-Sep-2016)

Ref Expression
Hypotheses alrimdd.1 ⊢ Ⅎ 𝑥 𝜑
alrimdd.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
alrimdd.3 ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion alrimdd ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜒 ) )

Proof

Step Hyp Ref Expression
1 alrimdd.1 ⊢ Ⅎ 𝑥 𝜑
2 alrimdd.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3 alrimdd.3 ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
4 2 nf5rd ⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜓 ) )
5 1 3 alimd ⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 → ∀ 𝑥 𝜒 ) )
6 4 5 syld ⊢ ( 𝜑 → ( 𝜓 → ∀ 𝑥 𝜒 ) )