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

Theorem alrimivv 1639
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
alrimivv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
alrimivv  |-  ( ph  ->  A. x A. y ps )
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)

Proof of Theorem alrimivv
StepHypRef Expression
1 alrimivv.1 . . 3  |-  ( ph  ->  ps )
21alrimiv 1638 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 1638 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546
This theorem is referenced by:  2ax17  1647  euind  3066  sbnfc2  3254  uniintsn  4031  ssopab2dv  4426  ordelord  4546  suctr  4607  eusvnf  4660  ssrel  4906  relssdv  4910  eqrelrdv  4914  eqbrrdv  4915  eqrelrdv2  4917  ssrelrel  4918  iss  5131  funssres  5435  funun  5437  fununi  5459  fsn  5847  wemoiso  6019  wemoiso2  6020  oprabexd  6127  ovg  6153  omeu  6766  qliftfund  6928  eroveu  6937  th3qlem1  6948  fpwwe2lem11  8450  seqf1o  11293  brfi1uzind  11644  summo  12440  pceu  13149  invfun  13918  psss  14575  spwmo  14587  gsumval3eu  15442  hausflimi  17935  vitalilem3  19371  plyexmo  20099  pjhthmo  22654  chscl  22993  cvmlift2lem12  24782  prodmo  25043  lineintmo  25807  trer  26012  unirep  26107  prter1  26421  ismrcd2  26446  ismrc  26448  psgneu  27100  rlimdmafv  27712  frgra3vlem1  27755  3vfriswmgralem  27759  truniALT  27971  gen12  28062  sspwtrALT  28278  sspwtrALT2  28279  suctrALT2  28292  trintALT  28336  suctrALTcf  28377  suctrALT3  28379  bnj1379  28542  bnj580  28624  bnj1321  28736  islpoldN  31601
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
  Copyright terms: Public domain W3C validator