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  3085  sbnfc2  3273  uniintsn  4051  ssopab2dv  4447  ordelord  4567  suctr  4628  eusvnf  4681  ssrel  4927  relssdv  4931  eqrelrdv  4935  eqbrrdv  4936  eqrelrdv2  4938  ssrelrel  4939  iss  5152  funssres  5456  funun  5458  fununi  5480  fsn  5869  wemoiso  6041  wemoiso2  6042  oprabexd  6149  ovg  6175  omeu  6791  qliftfund  6953  eroveu  6962  th3qlem1  6973  fpwwe2lem11  8475  seqf1o  11323  brfi1uzind  11674  summo  12470  pceu  13179  invfun  13948  psss  14605  spwmo  14617  gsumval3eu  15472  hausflimi  17969  vitalilem3  19459  plyexmo  20187  pjhthmo  22761  chscl  23100  cvmlift2lem12  24958  prodmo  25219  lineintmo  25999  mbfresfi  26156  trer  26213  unirep  26308  prter1  26622  ismrcd2  26647  ismrc  26649  psgneu  27301  rlimdmafv  27912  frgra3vlem1  28108  3vfriswmgralem  28112  frg2wot1  28164  2spotdisj  28168  truniALT  28341  gen12  28432  sspwtrALT  28648  sspwtrALT2  28649  suctrALT2  28662  trintALT  28706  suctrALTcf  28747  suctrALT3  28749  bnj1379  28912  bnj580  28994  bnj1321  29106  islpoldN  31971
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