Theorem 2ralimi 3126

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

Syntax hints:   → wi 4  ∀wral 3103

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

This theorem depends on definitions:  df-bi 208  df-ral 3108

This theorem is referenced by:  reusv3i  5189  ssrel2  5537  fununi  6291  fnmpo  7614  xpwdomg  8885  catcocl  16773  catpropd  16796  dfgrp3e  17944  rmodislmodlem  19379  rmodislmod  19380  tmdcn2  22369  xmeteq0  22619  xmettri2  22621  midf  26232  frgrconngr  27753  ajmoi  28314  adjmo  29288  cnlnssadj  29536  rngodi  34660  rngodir  34661  rngoass  34662  rngohomadd  34725  rngohommul  34726  ispridl2  34794  mpobi123f  34920  ntrk2imkb  39823  gneispaceel  39929  gneispacess  39931  stoweidlem60  41841