Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2ralimi Structured version   Visualization version   GIF version

Theorem 2ralimi 3129
 Description: Inference quantifying both antecedent and consequent two times, with strong hypothesis. (Contributed by AV, 3-Dec-2021.)
Hypothesis
Ref Expression
ralimi.1 (𝜑𝜓)
Assertion
Ref Expression
2ralimi (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)

Proof of Theorem 2ralimi
StepHypRef Expression
1 ralimi.1 . . 3 (𝜑𝜓)
21ralimi 3128 . 2 (∀𝑦𝐵 𝜑 → ∀𝑦𝐵 𝜓)
32ralimi 3128 1 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wral 3106 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 210  df-ral 3111 This theorem is referenced by:  reusv3i  5271  ssrel2  5624  fununi  6400  fnmpo  7752  xpwdomg  9036  catcocl  16951  catpropd  16974  dfgrp3e  18195  rmodislmodlem  19698  rmodislmod  19699  tmdcn2  22704  xmeteq0  22955  xmettri2  22957  midf  26580  frgrconngr  28089  ajmoi  28651  adjmo  29625  cnlnssadj  29873  prmidl2  31034  rngodi  35361  rngodir  35362  rngoass  35363  rngohomadd  35426  rngohommul  35427  ispridl2  35495  mpobi123f  35619  ntrk2imkb  40783  gneispaceel  40889  gneispacess  40891  stoweidlem60  42745
 Copyright terms: Public domain W3C validator