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

Theorem 2ralimi 3101
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 3100 . 2 (∀𝑦𝐵 𝜑 → ∀𝑦𝐵 𝜓)
32ralimi 3100 1 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884
This theorem depends on definitions:  df-bi 197  df-ral 3065
This theorem is referenced by:  reusv3i  5003  ssrel2  5350  fununi  6104  fnmpt2  7387  xpwdomg  8645  catcocl  16552  catpropd  16575  dfgrp3e  17722  rmodislmodlem  19139  rmodislmod  19140  tmdcn2  22112  xmeteq0  22362  xmettri2  22364  midf  25888  frgrconngr  27473  ajmoi  28048  adjmo  29025  cnlnssadj  29273  rngodi  34028  rngodir  34029  rngoass  34030  rngohomadd  34093  rngohommul  34094  ispridl2  34162  mpt2bi123f  34296  ntrk2imkb  38854  gneispaceel  38960  gneispacess  38962  stoweidlem60  40788
  Copyright terms: Public domain W3C validator