Theorem 2ralimi 3099

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

Syntax hints:   → wi 4  ∀wral 3044

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

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

This theorem is referenced by:  3ralimi  3100  reusv3i  5346  ssrel2  5732  fununi  6561  fnmpo  8011  xpwdomg  9496  catcocl  17609  catpropd  17633  dfgrp3e  18937  rmodislmodlem  20850  rmodislmod  20851  tmdcn2  23992  xmeteq0  24242  xmettri2  24244  mulsuniflem  28075  midf  28739  frgrconngr  30256  ajmoi  30820  adjmo  31794  cnlnssadj  32042  prmidl2  33388  rngodi  37883  rngodir  37884  rngoass  37885  rngohomadd  37948  rngohommul  37949  ispridl2  38017  mpobi123f  38141  ntrk2imkb  44010  gneispaceel  44116  gneispacess  44118  prclaxpr  44959  stoweidlem60  46042  fullthinc  49436  thincciso  49439