Theorem 2ralimi 3103

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

Syntax hints:   → wi 4  ∀wral 3044

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 3045

This theorem is referenced by:  3ralimi  3104  reusv3i  5359  ssrel2  5748  fununi  6591  fnmpo  8048  xpwdomg  9538  catcocl  17646  catpropd  17670  dfgrp3e  18972  rmodislmodlem  20835  rmodislmod  20836  tmdcn2  23976  xmeteq0  24226  xmettri2  24228  mulsuniflem  28052  midf  28703  frgrconngr  30223  ajmoi  30787  adjmo  31761  cnlnssadj  32009  prmidl2  33412  rngodi  37898  rngodir  37899  rngoass  37900  rngohomadd  37963  rngohommul  37964  ispridl2  38032  mpobi123f  38156  ntrk2imkb  44026  gneispaceel  44132  gneispacess  44134  prclaxpr  44975  stoweidlem60  46058  fullthinc  49439  thincciso  49442