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

Syntax hints:   → wi 4  ∀wral 3048

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 3049

This theorem is referenced by:  3ralimi  3104  reusv3i  5344  ssrel2  5729  fununi  6561  fnmpo  8007  xpwdomg  9478  catcocl  17593  catpropd  17617  dfgrp3e  18955  rmodislmodlem  20864  rmodislmod  20865  tmdcn2  24005  xmeteq0  24254  xmettri2  24256  mulsuniflem  28089  midf  28755  frgrconngr  30276  ajmoi  30840  adjmo  31814  cnlnssadj  32062  prmidl2  33413  rngodi  37964  rngodir  37965  rngoass  37966  rngohomadd  38029  rngohommul  38030  ispridl2  38098  mpobi123f  38222  ntrk2imkb  44154  gneispaceel  44260  gneispacess  44262  prclaxpr  45102  stoweidlem60  46182  fullthinc  49575  thincciso  49578