Theorem 2ralimi 3108

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

Syntax hints:   → wi 4  ∀wral 3052

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

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

This theorem is referenced by:  3ralimi  3109  reusv3i  5341  ssrel2  5734  fununi  6567  fnmpo  8015  xpwdomg  9493  catcocl  17642  catpropd  17666  dfgrp3e  19007  rmodislmodlem  20915  rmodislmod  20916  tmdcn2  24064  xmeteq0  24313  xmettri2  24315  mulsuniflem  28155  midf  28858  frgrconngr  30379  ajmoi  30944  adjmo  31918  cnlnssadj  32166  prmidl2  33516  rngodi  38239  rngodir  38240  rngoass  38241  rngohomadd  38304  rngohommul  38305  ispridl2  38373  mpobi123f  38497  disjimeceqim  39139  disjimrmoeqec  39143  ntrk2imkb  44482  gneispaceel  44588  gneispacess  44590  prclaxpr  45430  stoweidlem60  46506  fullthinc  49937  thincciso  49940