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

Theorem 2alimi 1804
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 1803 . 2 (∀𝑦𝜑 → ∀𝑦𝜓)
32alimi 1803 1 (∀𝑥𝑦𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-gen 1787  ax-4 1801
This theorem is referenced by:  alcomiw  2041  alcomiwOLD  2042  2mo  2726  2eu6  2737  euind  3712  reuind  3741  sbnfc2  4385  opelopabt  5410  ssrel  5650  ssrelrel  5662  fundif  6396  opabbrex  7196  fnoprabg  7264  tz7.48lem  8066  ssrelf  30294  bj-3exbi  33847  mpobi123f  35321  mptbi12f  35325  ismrc  39176  refimssco  39845  19.33-2  40591  pm11.63  40604  pm11.71  40606  axc5c4c711to11  40614  ichal  43504  ichan  43507
  Copyright terms: Public domain W3C validator