Theorem 2ralimi 3118

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

Syntax hints:   → wi 4  ∀wral 3056

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

This theorem depends on definitions:  df-bi 206  df-ral 3057

This theorem is referenced by:  3ralimi  3119  reusv3i  5398  ssrel2  5781  fununi  6622  fnmpo  8067  xpwdomg  9602  catcocl  17658  catpropd  17682  dfgrp3e  18989  rmodislmodlem  20805  rmodislmod  20806  rmodislmodOLD  20807  tmdcn2  23986  xmeteq0  24237  xmettri2  24239  mulsuniflem  28042  midf  28573  frgrconngr  30097  ajmoi  30661  adjmo  31635  cnlnssadj  31883  prmidl2  33146  rngodi  37366  rngodir  37367  rngoass  37368  rngohomadd  37431  rngohommul  37432  ispridl2  37500  mpobi123f  37624  ntrk2imkb  43439  gneispaceel  43545  gneispacess  43547  stoweidlem60  45420  fullthinc  48024  thincciso  48027