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

Theorem 2ralimi 3158
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 3157 . 2 (∀𝑦𝐵 𝜑 → ∀𝑦𝐵 𝜓)
32ralimi 3157 1 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-ral 3140
This theorem is referenced by:  reusv3i  5295  ssrel2  5652  fununi  6422  fnmpo  7756  xpwdomg  9037  catcocl  16944  catpropd  16967  dfgrp3e  18137  rmodislmodlem  19630  rmodislmod  19631  tmdcn2  22625  xmeteq0  22875  xmettri2  22877  midf  26489  frgrconngr  28000  ajmoi  28562  adjmo  29536  cnlnssadj  29784  prmidl2  30877  rngodi  35063  rngodir  35064  rngoass  35065  rngohomadd  35128  rngohommul  35129  ispridl2  35197  mpobi123f  35321  ntrk2imkb  40265  gneispaceel  40371  gneispacess  40373  stoweidlem60  42222
  Copyright terms: Public domain W3C validator