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  5347  ssrel2  5741  fununi  6574  fnmpo  8022  xpwdomg  9500  catcocl  17651  catpropd  17675  dfgrp3e  19016  rmodislmodlem  20924  rmodislmod  20925  tmdcn2  24054  xmeteq0  24303  xmettri2  24305  mulsuniflem  28141  midf  28844  frgrconngr  30364  ajmoi  30929  adjmo  31903  cnlnssadj  32151  prmidl2  33501  rngodi  38225  rngodir  38226  rngoass  38227  rngohomadd  38290  rngohommul  38291  ispridl2  38359  mpobi123f  38483  disjimeceqim  39125  disjimrmoeqec  39129  ntrk2imkb  44464  gneispaceel  44570  gneispacess  44572  prclaxpr  45412  stoweidlem60  46488  fullthinc  49919  thincciso  49922