Theorem 2ralimi 3087

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

Syntax hints:   → wi 4  ∀wral 3063

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

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

This theorem is referenced by:  reusv3i  5322  ssrel2  5685  fununi  6493  fnmpo  7882  xpwdomg  9274  catcocl  17311  catpropd  17335  dfgrp3e  18590  rmodislmodlem  20105  rmodislmod  20106  rmodislmodOLD  20107  tmdcn2  23148  xmeteq0  23399  xmettri2  23401  midf  27041  frgrconngr  28559  ajmoi  29121  adjmo  30095  cnlnssadj  30343  prmidl2  31518  xpord3ind  33727  rngodi  35989  rngodir  35990  rngoass  35991  rngohomadd  36054  rngohommul  36055  ispridl2  36123  mpobi123f  36247  ntrk2imkb  41536  gneispaceel  41642  gneispacess  41644  stoweidlem60  43491  fullthinc  46215  thincciso  46218