Theorem 2ralimi 3121

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

Syntax hints:   → wi 4  ∀wral 3059

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

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

This theorem is referenced by:  3ralimi  3122  reusv3i  5410  ssrel2  5798  fununi  6643  fnmpo  8093  xpwdomg  9623  catcocl  17730  catpropd  17754  dfgrp3e  19071  rmodislmodlem  20944  rmodislmod  20945  rmodislmodOLD  20946  tmdcn2  24113  xmeteq0  24364  xmettri2  24366  mulsuniflem  28190  midf  28799  frgrconngr  30323  ajmoi  30887  adjmo  31861  cnlnssadj  32109  prmidl2  33449  rngodi  37891  rngodir  37892  rngoass  37893  rngohomadd  37956  rngohommul  37957  ispridl2  38025  mpobi123f  38149  ntrk2imkb  44027  gneispaceel  44133  gneispacess  44135  prclaxpr  44948  stoweidlem60  46016  fullthinc  48846  thincciso  48849