Metamath Proof Explorer


Theorem ralimia

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 19-Jul-1996)

Ref Expression
Hypothesis ralimia.1 x A φ ψ
Assertion ralimia x A φ x A ψ

Proof

Step Hyp Ref Expression
1 ralimia.1 x A φ ψ
2 1 a2i x A φ x A ψ
3 2 ralimi2 x A φ x A ψ