Theorem 2ralimi 3104

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

Syntax hints:   → wi 4  ∀wral 3045

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 3046

This theorem is referenced by:  3ralimi  3105  reusv3i  5362  ssrel2  5751  fununi  6594  fnmpo  8051  xpwdomg  9545  catcocl  17653  catpropd  17677  dfgrp3e  18979  rmodislmodlem  20842  rmodislmod  20843  tmdcn2  23983  xmeteq0  24233  xmettri2  24235  mulsuniflem  28059  midf  28710  frgrconngr  30230  ajmoi  30794  adjmo  31768  cnlnssadj  32016  prmidl2  33419  rngodi  37905  rngodir  37906  rngoass  37907  rngohomadd  37970  rngohommul  37971  ispridl2  38039  mpobi123f  38163  ntrk2imkb  44033  gneispaceel  44139  gneispacess  44141  prclaxpr  44982  stoweidlem60  46065  fullthinc  49443  thincciso  49446