Theorem 2ralimi 3122

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

Syntax hints:   → wi 4  ∀wral 3060

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

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

This theorem is referenced by:  3ralimi  3123  reusv3i  5403  ssrel2  5794  fununi  6640  fnmpo  8095  xpwdomg  9626  catcocl  17729  catpropd  17753  dfgrp3e  19059  rmodislmodlem  20928  rmodislmod  20929  tmdcn2  24098  xmeteq0  24349  xmettri2  24351  mulsuniflem  28176  midf  28785  frgrconngr  30314  ajmoi  30878  adjmo  31852  cnlnssadj  32100  prmidl2  33470  rngodi  37912  rngodir  37913  rngoass  37914  rngohomadd  37977  rngohommul  37978  ispridl2  38046  mpobi123f  38170  ntrk2imkb  44055  gneispaceel  44161  gneispacess  44163  prclaxpr  45007  stoweidlem60  46080  fullthinc  49124  thincciso  49127