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

Theorem 2alimi 1907
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 1906 . 2 (∀𝑦𝜑 → ∀𝑦𝜓)
32alimi 1906 1 (∀𝑥𝑦𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1650
This theorem was proved from axioms:  ax-mp 5  ax-gen 1890  ax-4 1904
This theorem is referenced by:  alcomiw  2138  2mo  2673  2eu6  2680  euind  3554  reuind  3574  sbnfc2  4171  opelopabt  5150  ssrel  5379  ssrelrel  5391  fundif  6118  opabbrex  6897  fnoprabg  6963  tz7.48lem  7744  ssrelf  29896  bj-3exbi  33057  bj-mo3OLD  33282  mpt2bi123f  34413  mptbi12f  34417  ismrc  37966  refimssco  38612  19.33-2  39279  pm11.63  39293  pm11.71  39295  axc5c4c711to11  39303
  Copyright terms: Public domain W3C validator