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 ) |
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 ) |