Theorem 2ralimi 3129

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

Syntax hints:   → wi 4  ∀wral 3067

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

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

This theorem is referenced by:  3ralimi  3130  reusv3i  5422  ssrel2  5809  fununi  6653  fnmpo  8110  xpwdomg  9654  catcocl  17743  catpropd  17767  dfgrp3e  19080  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  tmdcn2  24118  xmeteq0  24369  xmettri2  24371  mulsuniflem  28193  midf  28802  frgrconngr  30326  ajmoi  30890  adjmo  31864  cnlnssadj  32112  prmidl2  33434  rngodi  37864  rngodir  37865  rngoass  37866  rngohomadd  37929  rngohommul  37930  ispridl2  37998  mpobi123f  38122  ntrk2imkb  43999  gneispaceel  44105  gneispacess  44107  stoweidlem60  45981  fullthinc  48713  thincciso  48716