Theorem 2ralimi 3088

Description: Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.)

Hypothesis

Ref	Expression
ralimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
2ralimi	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Proof of Theorem 2ralimi

Step	Hyp	Ref	Expression
1		ralimi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	ralimi 3087	. 2 ⊢ (∀𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ 𝐵 𝜓)
3	2	ralimi 3087	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)

Syntax hints:   → wi 4  ∀wral 3064

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

This theorem depends on definitions:  df-bi 206  df-ral 3069

This theorem is referenced by:  reusv3i  5327  ssrel2  5696  fununi  6509  fnmpo  7909  xpwdomg  9344  catcocl  17394  catpropd  17418  dfgrp3e  18675  rmodislmodlem  20190  rmodislmod  20191  rmodislmodOLD  20192  tmdcn2  23240  xmeteq0  23491  xmettri2  23493  midf  27137  frgrconngr  28658  ajmoi  29220  adjmo  30194  cnlnssadj  30442  prmidl2  31616  xpord3ind  33800  rngodi  36062  rngodir  36063  rngoass  36064  rngohomadd  36127  rngohommul  36128  ispridl2  36196  mpobi123f  36320  ntrk2imkb  41647  gneispaceel  41753  gneispacess  41755  stoweidlem60  43601  fullthinc  46327  thincciso  46330