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

Theorem 2alimi 1809
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 1808 . 2 (∀𝑦𝜑 → ∀𝑦𝜓)
32alimi 1808 1 (∀𝑥𝑦𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1535
This theorem was proved from axioms:  ax-mp 5  ax-gen 1792  ax-4 1806
This theorem is referenced by:  alcomimw  2040  2mo  2646  2eu6  2655  euind  3733  reuind  3762  sbnfc2  4445  opelopabt  5542  ssrel  5795  ssrelOLD  5796  ssrelrel  5809  fundif  6617  opabbrex  7484  fnoprabg  7556  tz7.48lem  8480  ssrelf  32635  bj-3exbi  36599  mpobi123f  38149  mptbi12f  38153  ismrc  42689  refimssco  43597  19.33-2  44378  pm11.63  44391  pm11.71  44393  axc5c4c711to11  44401  ichal  47391
  Copyright terms: Public domain W3C validator