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

Theorem 2alimi 1606
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 1605 . 2  |-  ( A. y ph  ->  A. y ps )
32alimi 1605 1  |-  ( A. x A. y ph  ->  A. x A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1368
This theorem was proved from axioms:  ax-mp 5  ax-gen 1592  ax-4 1603
This theorem is referenced by:  mo3OLD  2305  moOLD  2311  2mo  2366  2moOLD  2367  2moOLDOLD  2368  2eu6  2377  2eu6OLD  2378  euind  3229  reuind  3246  sbnfc2  3790  opelopabt  4685  ssrel  5012  ssrelrel  5024  fnoprabg  6277  tz7.48lem  6982  ssrelf  26065  mpt2bi123f  29099  mptbi12f  29103  ismrc  29161  19.33-2  29758  pm11.63  29772  pm11.71  29774  axc5c4c711to11  29783  bj-3exbi  32430
  Copyright terms: Public domain W3C validator