Theorem 2ralimi 3110

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

Syntax hints:   → wi 4  ∀wral 3054

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

This theorem depends on definitions:  df-bi 208  df-ral 3055

This theorem is referenced by:  3ralimi  3111  reusv3i  5340  ssrel2  5735  fununi  6567  fnmpo  8018  xpwdomg  9497  catcocl  17649  catpropd  17673  dfgrp3e  19014  rmodislmodlem  20926  rmodislmod  20927  tmdcn2  24079  xmeteq0  24328  xmettri2  24330  mulsuniflem  28166  midf  28869  frgrconngr  30389  ajmoi  30954  adjmo  31928  cnlnssadj  32176  prmidl2  33531  rngodi  38278  rngodir  38279  rngoass  38280  rngohomadd  38343  rngohommul  38344  ispridl2  38412  mpobi123f  38536  disjimeceqim  39178  disjimrmoeqec  39182  ntrk2imkb  44488  gneispaceel  44594  gneispacess  44596  prclaxpr  45436  stoweidlem60  46510  fullthinc  49947  thincciso  49950