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

Theorem 2ralimi 3126
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 3125 . 2 (∀𝑦𝐵 𝜑 → ∀𝑦𝐵 𝜓)
32ralimi 3125 1 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 3103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789
This theorem depends on definitions:  df-bi 208  df-ral 3108
This theorem is referenced by:  reusv3i  5189  ssrel2  5537  fununi  6291  fnmpo  7614  xpwdomg  8885  catcocl  16773  catpropd  16796  dfgrp3e  17944  rmodislmodlem  19379  rmodislmod  19380  tmdcn2  22369  xmeteq0  22619  xmettri2  22621  midf  26232  frgrconngr  27753  ajmoi  28314  adjmo  29288  cnlnssadj  29536  rngodi  34660  rngodir  34661  rngoass  34662  rngohomadd  34725  rngohommul  34726  ispridl2  34794  mpobi123f  34920  ntrk2imkb  39823  gneispaceel  39929  gneispacess  39931  stoweidlem60  41841
  Copyright terms: Public domain W3C validator