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

Theorem 2alimi 1737
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 1736 . 2 (∀𝑦𝜑 → ∀𝑦𝜓)
32alimi 1736 1 (∀𝑥𝑦𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1478
This theorem was proved from axioms:  ax-mp 5  ax-gen 1719  ax-4 1734
This theorem is referenced by:  2mo  2550  2eu6  2557  euind  3375  reuind  3393  sbnfc2  3979  opelopabt  4947  ssrel  5168  ssrelOLD  5169  ssrelrel  5181  fundif  5893  opabbrex  6648  fnoprabg  6714  tz7.48lem  7481  ssrelf  29268  bj-3exbi  32242  bj-mo3OLD  32477  mpt2bi123f  33603  mptbi12f  33607  ismrc  36744  refimssco  37394  19.33-2  38063  pm11.63  38077  pm11.71  38079  axc5c4c711to11  38088
  Copyright terms: Public domain W3C validator