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

Theorem 2alimi 1811
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 1810 . 2 (∀𝑦𝜑 → ∀𝑦𝜓)
32alimi 1810 1 (∀𝑥𝑦𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1537
This theorem was proved from axioms:  ax-mp 5  ax-gen 1794  ax-4 1808
This theorem is referenced by:  alcomimw  2041  2mo  2647  2eu6  2656  euind  3729  reuind  3758  sbnfc2  4438  opelopabt  5536  ssrel  5791  ssrelOLD  5792  ssrelrel  5805  fundif  6614  opabbrex  7485  fnoprabg  7557  tz7.48lem  8482  ssrelf  32628  bj-3exbi  36618  mpobi123f  38170  mptbi12f  38174  ismrc  42717  refimssco  43625  19.33-2  44406  pm11.63  44419  pm11.71  44421  axc5c4c711to11  44429  ichal  47458
  Copyright terms: Public domain W3C validator