Metamath Proof Explorer

Theorem ralrimi

Description: Inference from Theorem 19.21 of Margaris p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999) Shortened after introduction of hbralrimi . (Revised by Wolf Lammen, 4-Dec-2019)

Ref Expression
Hypotheses ralrimi.1 x φ
ralrimi.2 φ x A ψ
Assertion ralrimi φ x A ψ


Step Hyp Ref Expression
1 ralrimi.1 x φ
2 ralrimi.2 φ x A ψ
3 1 nf5ri φ x φ
4 3 2 hbralrimi φ x A ψ