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

Theorem 2ralimi 3118
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 3078 . 2 (∀𝑦𝐵 𝜑 → ∀𝑦𝐵 𝜓)
32ralimi 3078 1 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wral 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-ral 3057
This theorem is referenced by:  3ralimi  3119  reusv3i  5398  ssrel2  5781  fununi  6622  fnmpo  8067  xpwdomg  9602  catcocl  17658  catpropd  17682  dfgrp3e  18989  rmodislmodlem  20805  rmodislmod  20806  rmodislmodOLD  20807  tmdcn2  23986  xmeteq0  24237  xmettri2  24239  mulsuniflem  28042  midf  28573  frgrconngr  30097  ajmoi  30661  adjmo  31635  cnlnssadj  31883  prmidl2  33146  rngodi  37366  rngodir  37367  rngoass  37368  rngohomadd  37431  rngohommul  37432  ispridl2  37500  mpobi123f  37624  ntrk2imkb  43439  gneispaceel  43545  gneispacess  43547  stoweidlem60  45420  fullthinc  48024  thincciso  48027
  Copyright terms: Public domain W3C validator