Theorem 2ralimi 3124

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

Hypothesis

Ref	Expression
2ralimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
2ralimi	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2ralimi

Step	Hyp	Ref	Expression
1		2ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ralimi 3084	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralimi 3084	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  3ralimi  3125  reusv3i  5403  ssrel2  5786  fununi  6624  fnmpo  8055  xpwdomg  9580  catcocl  17629  catpropd  17653  dfgrp3e  18923  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  tmdcn2  23593  xmeteq0  23844  xmettri2  23846  mulsuniflem  27607  midf  28058  frgrconngr  29578  ajmoi  30142  adjmo  31116  cnlnssadj  31364  prmidl2  32590  rngodi  36820  rngodir  36821  rngoass  36822  rngohomadd  36885  rngohommul  36886  ispridl2  36954  mpobi123f  37078  ntrk2imkb  42836  gneispaceel  42942  gneispacess  42944  stoweidlem60  44824  fullthinc  47714  thincciso  47717