Theorem 2ralimi 3110

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 3073	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralimi 3073	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4  ∀wral 3051

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

This theorem depends on definitions:  df-bi 207  df-ral 3052

This theorem is referenced by:  3ralimi  3111  reusv3i  5374  ssrel2  5764  fununi  6610  fnmpo  8066  xpwdomg  9597  catcocl  17695  catpropd  17719  dfgrp3e  19021  rmodislmodlem  20884  rmodislmod  20885  tmdcn2  24025  xmeteq0  24275  xmettri2  24277  mulsuniflem  28092  midf  28701  frgrconngr  30221  ajmoi  30785  adjmo  31759  cnlnssadj  32007  prmidl2  33402  rngodi  37874  rngodir  37875  rngoass  37876  rngohomadd  37939  rngohommul  37940  ispridl2  38008  mpobi123f  38132  ntrk2imkb  44008  gneispaceel  44114  gneispacess  44116  prclaxpr  44958  stoweidlem60  46037  fullthinc  49284  thincciso  49287