Theorem hbralrimi 3154

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3262 and ralrimiv 3155. Its main advantage over these two is its minimal references to axioms. The proof is extracted from NM's previous work. (Contributed by Wolf Lammen, 4-Dec-2019.)

Hypotheses

Ref	Expression
hbralrimi.1	⊢ (𝜑 → ∀𝑥𝜑)
hbralrimi.2	⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))

Assertion

Ref	Expression
hbralrimi	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem hbralrimi

Step	Hyp	Ref	Expression
1		hbralrimi.1	. . 3 ⊢ (𝜑 → ∀𝑥𝜑)
2		hbralrimi.2	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
3	1, 2	alrimih 1846	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4	3	ralrid 3086	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  ∀wal 1560   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831

This theorem depends on definitions:  df-bi 209  df-ral 3079

This theorem is referenced by:  ralrimiv  3155  ralrimi  3262  bnj1145  35290