Theorem 2ralimi 3135

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

Syntax hints:   → wi 4  ∀wral 3079

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

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  3ralimi  3136  reusv3i  5377  ssrel2  5773  fununi  6613  fnmpo  8067  xpwdomg  9548  catcocl  17742  catpropd  17766  dfgrp3e  19107  rmodislmodlem  21031  rmodislmod  21032  prmidl2  21447  tmdcn2  24227  xmeteq0  24476  xmettri2  24478  mulsuniflem  28320  midf  29063  frgrconngr  30623  ajmoi  31188  adjmo  32162  cnlnssadj  32410  nmulprop  36660  rngodi  38533  rngodir  38534  rngoass  38535  rngohomadd  38598  rngohommul  38599  ispridl2  38667  mpobi123f  38789  disjimeceqim  39431  disjimrmoeqec  39435  ntrk2imkb  44743  gneispaceel  44849  gneispacess  44851  prclaxpr  45674  stoweidlem60  46754  fullthinc  50205  thincciso  50208