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  27604  midf  28027  frgrconngr  29547  ajmoi  30111  adjmo  31085  cnlnssadj  31333  prmidl2  32559  rngodi  36772  rngodir  36773  rngoass  36774  rngohomadd  36837  rngohommul  36838  ispridl2  36906  mpobi123f  37030  ntrk2imkb  42788  gneispaceel  42894  gneispacess  42896  stoweidlem60  44776  fullthinc  47666  thincciso  47669