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

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

Proof of Theorem 2ralimi
StepHypRef Expression
1 2ralimi.1 . . 3 (𝜑𝜓)
21ralimi 3082 . 2 (∀𝑦𝐵 𝜑 → ∀𝑦𝐵 𝜓)
32ralimi 3082 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 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-ral 3061
This theorem is referenced by:  3ralimi  3123  reusv3i  5403  ssrel2  5794  fununi  6640  fnmpo  8095  xpwdomg  9626  catcocl  17729  catpropd  17753  dfgrp3e  19059  rmodislmodlem  20928  rmodislmod  20929  tmdcn2  24098  xmeteq0  24349  xmettri2  24351  mulsuniflem  28176  midf  28785  frgrconngr  30314  ajmoi  30878  adjmo  31852  cnlnssadj  32100  prmidl2  33470  rngodi  37912  rngodir  37913  rngoass  37914  rngohomadd  37977  rngohommul  37978  ispridl2  38046  mpobi123f  38170  ntrk2imkb  44055  gneispaceel  44161  gneispacess  44163  prclaxpr  45007  stoweidlem60  46080  fullthinc  49124  thincciso  49127
  Copyright terms: Public domain W3C validator