Theorem 2ralimi 2953

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

Hypothesis

Ref	Expression
ralimi.1	|- ( ph -> ps )

Assertion

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

Proof of Theorem 2ralimi

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

Syntax hints:   -> wi 4   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  reusv3i  4875  ssrel2  5210  fununi  5964  fnmpt2  7238  xpwdomg  8490  catcocl  16346  catpropd  16369  dfgrp3e  17515  rmodislmodlem  18930  rmodislmod  18931  tmdcn2  21893  xmeteq0  22143  xmettri2  22145  midf  25668  frgrconngr  27158  ajmoi  27714  adjmo  28691  cnlnssadj  28939  rngodi  33703  rngodir  33704  rngoass  33705  rngohomadd  33768  rngohommul  33769  ispridl2  33837  mpt2bi123f  33971  ntrk2imkb  38335  gneispaceel  38441  gneispacess  38443  stoweidlem60  40277