Metamath Proof Explorer


Theorem 4ralimi

Description: Inference quantifying both antecedent and consequent four times, with strong hypothesis. (Contributed by Scott Fenton, 5-Mar-2025)

Ref Expression
Hypothesis 2ralimi.1
|- ( ph -> ps )
Assertion 4ralimi
|- ( A. x e. A A. y e. B A. z e. C A. w e. D ph -> A. x e. A A. y e. B A. z e. C A. w e. D ps )

Proof

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