Metamath Proof Explorer


Theorem 2ralimi

Description: Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021)

Ref Expression
Hypothesis ralimi.1 φ ψ
Assertion 2ralimi x A y B φ x A y B ψ

Proof

Step Hyp Ref Expression
1 ralimi.1 φ ψ
2 1 ralimi y B φ y B ψ
3 2 ralimi x A y B φ x A y B ψ