Theorem 2ralimi 3108

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

Syntax hints:   → wi 4  ∀wral 3052

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

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

This theorem is referenced by:  3ralimi  3109  reusv3i  5351  ssrel2  5742  fununi  6575  fnmpo  8023  xpwdomg  9502  catcocl  17620  catpropd  17644  dfgrp3e  18982  rmodislmodlem  20892  rmodislmod  20893  tmdcn2  24045  xmeteq0  24294  xmettri2  24296  mulsuniflem  28157  midf  28860  frgrconngr  30381  ajmoi  30945  adjmo  31919  cnlnssadj  32167  prmidl2  33533  rngodi  38149  rngodir  38150  rngoass  38151  rngohomadd  38214  rngohommul  38215  ispridl2  38283  mpobi123f  38407  disjimeceqim  39049  disjimrmoeqec  39053  ntrk2imkb  44387  gneispaceel  44493  gneispacess  44495  prclaxpr  45335  stoweidlem60  46412  fullthinc  49803  thincciso  49806