Theorem 2ralimi 3132

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

This proof depends on syntax axioms:   → wi 4  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  3ralimi  3133  reusv3i  5365  ssrel2  5760  fununi  6615  fnmpo  8080  ovmptss  8104  xpwdomg  9582  catcocl  17864  catpropd  17888  dfgrp3e  19255  rmodislmodlem  21209  rmodislmod  21210  prmidl2  21627  tmdcn2  24413  xmeteq0  24662  xmettri2  24664  mulsuniflem  28540  midf  29286  frgrconngr  30900  ajmoi  31465  adjmo  32439  cnlnssadj  32687  nmulprop  37031  rngodi  38931  rngodir  38932  rngoass  38933  rngohomadd  38996  rngohommul  38997  ispridl2  39065  mpobi123f  39187  disjimeceqim  39829  disjimrmoeqec  39833  ntrk2imkb  45130  gneispaceel  45236  gneispacess  45238  prclaxpr  46068  stoweidlem60  47163  fullthinc  50678  thincciso  50681