Theorem 2ralimi 3134

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

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

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

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

This theorem is used by:  3ralimi  3135  reusv3i  5373  ssrel2  5769  fununi  6612  fnmpo  8070  xpwdomg  9561  catcocl  17779  catpropd  17803  dfgrp3e  19169  rmodislmodlem  21119  rmodislmod  21120  prmidl2  21535  tmdcn2  24321  xmeteq0  24570  xmettri2  24572  mulsuniflem  28422  midf  29168  frgrconngr  30782  ajmoi  31347  adjmo  32321  cnlnssadj  32569  nmulprop  36778  rngodi  38662  rngodir  38663  rngoass  38664  rngohomadd  38727  rngohommul  38728  ispridl2  38796  mpobi123f  38918  disjimeceqim  39560  disjimrmoeqec  39564  ntrk2imkb  44885  gneispaceel  44991  gneispacess  44993  prclaxpr  45816  stoweidlem60  46896  fullthinc  50384  thincciso  50387