Theorem 2ralimi 3136

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

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

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 3081

This theorem is used by:  3ralimi  3137  reusv3i  5370  ssrel2  5766  fununi  6637  fnmpo  8105  ovmptss  8129  xpwdomg  9606  catcocl  17888  catpropd  17912  dfgrp3e  19279  rmodislmodlem  21234  rmodislmod  21235  prmidl2  21652  tmdcn2  24438  xmeteq0  24687  xmettri2  24689  mulsuniflem  28565  midf  29311  frgrconngr  30925  ajmoi  31490  adjmo  32464  cnlnssadj  32712  nmulprop  37117  rngodi  39030  rngodir  39031  rngoass  39032  rngohomadd  39095  rngohommul  39096  ispridl2  39164  mpobi123f  39286  disjimeceqim  39928  disjimrmoeqec  39932  ntrk2imkb  45229  gneispaceel  45335  gneispacess  45337  prclaxpr  46170  stoweidlem60  47275  fullthinc  50790  thincciso  50793