Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  hbralrimi Structured version   Visualization version   GIF version

Theorem hbralrimi 3092
 Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3095 and ralrimiv 3103. 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
StepHypRef Expression
1 hbralrimi.1 . . 3 (𝜑 → ∀𝑥𝜑)
2 hbralrimi.2 . . 3 (𝜑 → (𝑥𝐴𝜓))
31, 2alrimih 1900 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3055 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
53, 4sylibr 224 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1630   ∈ wcel 2139  ∀wral 3050 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886 This theorem depends on definitions:  df-bi 197  df-ral 3055 This theorem is referenced by:  ralrimi  3095  ralrimiv  3103  bnj1145  31389
 Copyright terms: Public domain W3C validator