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

Theorem 2alimi 1806
Description: Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
Hypothesis
Ref Expression
alimi.1 (𝜑𝜓)
Assertion
Ref Expression
2alimi (∀𝑥𝑦𝜑 → ∀𝑥𝑦𝜓)

Proof of Theorem 2alimi
StepHypRef Expression
1 alimi.1 . . 3 (𝜑𝜓)
21alimi 1805 . 2 (∀𝑦𝜑 → ∀𝑦𝜓)
32alimi 1805 1 (∀𝑥𝑦𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531
This theorem was proved from axioms:  ax-mp 5  ax-gen 1789  ax-4 1803
This theorem is referenced by:  alcomiw  2038  2mo  2636  2eu6  2645  euind  3716  reuind  3745  sbnfc2  4438  opelopabt  5534  ssrel  5784  ssrelOLD  5785  ssrelrel  5798  fundif  6603  opabbrex  7471  fnoprabg  7543  tz7.48lem  8462  ssrelf  32484  bj-3exbi  36221  mpobi123f  37763  mptbi12f  37767  ismrc  42260  refimssco  43176  19.33-2  43958  pm11.63  43971  pm11.71  43973  axc5c4c711to11  43981  ichal  46940
  Copyright terms: Public domain W3C validator