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

Theorem 2alimi 1780
 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 1779 . 2 (∀𝑦𝜑 → ∀𝑦𝜓)
32alimi 1779 1 (∀𝑥𝑦𝜑 → ∀𝑥𝑦𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1521 This theorem was proved from axioms:  ax-mp 5  ax-gen 1762  ax-4 1777 This theorem is referenced by:  2mo  2580  2eu6  2587  euind  3426  reuind  3444  sbnfc2  4040  opelopabt  5016  ssrel  5241  ssrelOLD  5242  ssrelrel  5254  fundif  5973  opabbrex  6737  fnoprabg  6803  tz7.48lem  7581  ssrelf  29553  bj-3exbi  32725  bj-mo3OLD  32957  mpt2bi123f  34101  mptbi12f  34105  ismrc  37581  refimssco  38230  19.33-2  38898  pm11.63  38912  pm11.71  38914  axc5c4c711to11  38923
 Copyright terms: Public domain W3C validator