Theorem 2ralimi 3135

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

Syntax hints:   → wi 4  ∀wral 3079

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

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  3ralimi  3136  reusv3i  5366  ssrel2  5762  fununi  6600  fnmpo  8054  xpwdomg  9535  catcocl  17731  catpropd  17755  dfgrp3e  19097  rmodislmodlem  21019  rmodislmod  21020  prmidl2  21428  tmdcn2  24207  xmeteq0  24456  xmettri2  24458  mulsuniflem  28300  midf  29028  frgrconngr  30554  ajmoi  31119  adjmo  32093  cnlnssadj  32341  nmulprop  36553  rngodi  38415  rngodir  38416  rngoass  38417  rngohomadd  38480  rngohommul  38481  ispridl2  38549  mpobi123f  38673  disjimeceqim  39315  disjimrmoeqec  39319  ntrk2imkb  44625  gneispaceel  44731  gneispacess  44733  prclaxpr  45559  stoweidlem60  46632  fullthinc  50079  thincciso  50082