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

Theorem 2alimi 1649
Description: Inference doubly quantifying both antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
Hypothesis
Ref Expression
alimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
2alimi  |-  ( A. x A. y ph  ->  A. x A. y ps )

Proof of Theorem 2alimi
StepHypRef Expression
1 alimi.1 . . 3  |-  ( ph  ->  ps )
21alimi 1648 . 2  |-  ( A. y ph  ->  A. y ps )
32alimi 1648 1  |-  ( A. x A. y ph  ->  A. x A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1397
This theorem was proved from axioms:  ax-mp 5  ax-gen 1633  ax-4 1646
This theorem is referenced by:  mo3OLD  2273  2mo  2318  2moOLD  2319  2eu6  2328  2eu6OLD  2329  euind  3228  reuind  3245  sbnfc2  3791  opelopabt  4690  ssrel  5021  ssrelrel  5033  opabbrex  6260  fnoprabg  6324  tz7.48lem  7046  ssrelf  27634  mpt2bi123f  30777  mptbi12f  30781  ismrc  30839  19.33-2  31495  pm11.63  31509  pm11.71  31511  axc5c4c711to11  31520  bj-3exbi  34593
  Copyright terms: Public domain W3C validator