Theorem 2ralimi 3131

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

Syntax hints:   → wi 4  ∀wral 3075

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

This theorem depends on definitions:  df-bi 209  df-ral 3076

This theorem is referenced by:  3ralimi  3132  reusv3i  5360  ssrel2  5755  fununi  6592  fnmpo  8046  xpwdomg  9530  catcocl  17700  catpropd  17724  dfgrp3e  19065  rmodislmodlem  20976  rmodislmod  20977  tmdcn2  24129  xmeteq0  24378  xmettri2  24380  mulsuniflem  28219  midf  28922  frgrconngr  30442  ajmoi  31007  adjmo  31981  cnlnssadj  32229  prmidl2  33588  nmulprop  36504  rngodi  38367  rngodir  38368  rngoass  38369  rngohomadd  38432  rngohommul  38433  ispridl2  38501  mpobi123f  38625  disjimeceqim  39267  disjimrmoeqec  39271  ntrk2imkb  44577  gneispaceel  44683  gneispacess  44685  prclaxpr  45525  stoweidlem60  46598  fullthinc  50035  thincciso  50038