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	|- ( ph -> ps )
Assertion	2ralimi	|- ( A. x e. A A. y e. B ph -> A. x e. A A. y e. B ps )

Proof

Step	Hyp	Ref	Expression
1		ralimi.1	|- ( ph -> ps )
2	1	ralimi	|- ( A. y e. B ph -> A. y e. B ps )
3	2	ralimi	|- ( A. x e. A A. y e. B ph -> A. x e. A A. y e. B ps )