Theorem 2ralimi 3111

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 3074	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralimi 3074	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 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-ral 3053

This theorem is referenced by:  3ralimi  3112  reusv3i  5379  ssrel2  5769  fununi  6616  fnmpo  8073  xpwdomg  9604  catcocl  17702  catpropd  17726  dfgrp3e  19028  rmodislmodlem  20891  rmodislmod  20892  tmdcn2  24032  xmeteq0  24282  xmettri2  24284  mulsuniflem  28109  midf  28760  frgrconngr  30280  ajmoi  30844  adjmo  31818  cnlnssadj  32066  prmidl2  33461  rngodi  37933  rngodir  37934  rngoass  37935  rngohomadd  37998  rngohommul  37999  ispridl2  38067  mpobi123f  38191  ntrk2imkb  44028  gneispaceel  44134  gneispacess  44136  prclaxpr  44977  stoweidlem60  46056  fullthinc  49303  thincciso  49306