Theorem 2ralimi 3133

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

This proof depends on syntax axioms:   → wi 4  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3078

This theorem is used by:  3ralimi  3134  reusv3i  5366  ssrel2  5761  fununi  6607  fnmpo  8069  xpwdomg  9563  catcocl  17839  catpropd  17863  dfgrp3e  19230  rmodislmodlem  21184  rmodislmod  21185  prmidl2  21602  tmdcn2  24388  xmeteq0  24637  xmettri2  24639  mulsuniflem  28517  midf  29263  frgrconngr  30877  ajmoi  31442  adjmo  32416  cnlnssadj  32664  nmulprop  36909  rngodi  38806  rngodir  38807  rngoass  38808  rngohomadd  38871  rngohommul  38872  ispridl2  38940  mpobi123f  39062  disjimeceqim  39704  disjimrmoeqec  39708  ntrk2imkb  44996  gneispaceel  45102  gneispacess  45104  prclaxpr  45927  stoweidlem60  47014  fullthinc  50502  thincciso  50505