Theorem 2ralimi 3101

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

Syntax hints:   → wi 4  ∀wral 3060

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

This theorem depends on definitions:  df-bi 197  df-ral 3065

This theorem is referenced by:  reusv3i  5003  ssrel2  5350  fununi  6104  fnmpt2  7387  xpwdomg  8645  catcocl  16552  catpropd  16575  dfgrp3e  17722  rmodislmodlem  19139  rmodislmod  19140  tmdcn2  22112  xmeteq0  22362  xmettri2  22364  midf  25888  frgrconngr  27473  ajmoi  28048  adjmo  29025  cnlnssadj  29273  rngodi  34028  rngodir  34029  rngoass  34030  rngohomadd  34093  rngohommul  34094  ispridl2  34162  mpt2bi123f  34296  ntrk2imkb  38854  gneispaceel  38960  gneispacess  38962  stoweidlem60  40788