Theorem 2ralimi 3106

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 1796  ax-4 1810

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

This theorem is referenced by:  3ralimi  3107  reusv3i  5349  ssrel2  5734  fununi  6567  fnmpo  8013  xpwdomg  9490  catcocl  17608  catpropd  17632  dfgrp3e  18970  rmodislmodlem  20880  rmodislmod  20881  tmdcn2  24033  xmeteq0  24282  xmettri2  24284  mulsuniflem  28145  midf  28848  frgrconngr  30369  ajmoi  30933  adjmo  31907  cnlnssadj  32155  prmidl2  33522  rngodi  38101  rngodir  38102  rngoass  38103  rngohomadd  38166  rngohommul  38167  ispridl2  38235  mpobi123f  38359  ntrk2imkb  44274  gneispaceel  44380  gneispacess  44382  prclaxpr  45222  stoweidlem60  46300  fullthinc  49691  thincciso  49694