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

Theorem 2alimi 1807
 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 1806 . 2 (∀𝑦𝜑 → ∀𝑦𝜓)
32alimi 1806 1 (∀𝑥𝑦𝜑 → ∀𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1529 This theorem was proved from axioms:  ax-mp 5  ax-gen 1790  ax-4 1804 This theorem is referenced by:  alcomiw  2044  alcomiwOLD  2045  2mo  2727  2eu6  2738  euind  3713  reuind  3742  sbnfc2  4386  opelopabt  5410  ssrel  5650  ssrelrel  5662  fundif  6396  opabbrex  7199  fnoprabg  7267  tz7.48lem  8069  ssrelf  30358  bj-3exbi  33943  mpobi123f  35432  mptbi12f  35436  ismrc  39288  refimssco  39957  19.33-2  40704  pm11.63  40717  pm11.71  40719  axc5c4c711to11  40727  ichal  43617  ichan  43620
 Copyright terms: Public domain W3C validator