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

Theorem 2ralimi 3102
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 3101 . 2 (∀𝑦𝐵 𝜑 → ∀𝑦𝐵 𝜓)
32ralimi 3101 1 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-ral 3066
This theorem is referenced by:  reusv3i  5005  ssrel2  5349  fununi  6103  fnmpt2  7392  xpwdomg  8650  catcocl  16553  catpropd  16576  dfgrp3e  17723  rmodislmodlem  19140  rmodislmod  19141  tmdcn2  22113  xmeteq0  22363  xmettri2  22365  midf  25889  frgrconngr  27476  ajmoi  28054  adjmo  29031  cnlnssadj  29279  rngodi  34033  rngodir  34034  rngoass  34035  rngohomadd  34098  rngohommul  34099  ispridl2  34167  mpt2bi123f  34301  ntrk2imkb  38859  gneispaceel  38965  gneispacess  38967  stoweidlem60  40789
  Copyright terms: Public domain W3C validator