Theorem 2ralimi 3102

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

Syntax hints:   → wi 4  ∀wral 3047

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

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

This theorem is referenced by:  3ralimi  3103  reusv3i  5342  ssrel2  5725  fununi  6556  fnmpo  8001  xpwdomg  9471  catcocl  17588  catpropd  17612  dfgrp3e  18950  rmodislmodlem  20860  rmodislmod  20861  tmdcn2  24002  xmeteq0  24251  xmettri2  24253  mulsuniflem  28086  midf  28752  frgrconngr  30269  ajmoi  30833  adjmo  31807  cnlnssadj  32055  prmidl2  33401  rngodi  37943  rngodir  37944  rngoass  37945  rngohomadd  38008  rngohommul  38009  ispridl2  38077  mpobi123f  38201  ntrk2imkb  44069  gneispaceel  44175  gneispacess  44177  prclaxpr  45017  stoweidlem60  46097  fullthinc  49481  thincciso  49484