Theorem 2ralimi 3138

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

This proof depends on syntax axioms:   → wi 4  ∀wral 3082

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3083

This theorem is used by:  3ralimi  3139  reusv3i  5380  ssrel2  5776  fununi  6618  fnmpo  8075  xpwdomg  9557  catcocl  17766  catpropd  17790  dfgrp3e  19137  rmodislmodlem  21087  rmodislmod  21088  prmidl2  21503  tmdcn2  24283  xmeteq0  24532  xmettri2  24534  mulsuniflem  28379  midf  29122  frgrconngr  30682  ajmoi  31247  adjmo  32221  cnlnssadj  32469  nmulprop  36702  rngodi  38595  rngodir  38596  rngoass  38597  rngohomadd  38660  rngohommul  38661  ispridl2  38729  mpobi123f  38851  disjimeceqim  39493  disjimrmoeqec  39497  ntrk2imkb  44803  gneispaceel  44909  gneispacess  44911  prclaxpr  45734  stoweidlem60  46814  fullthinc  50268  thincciso  50271