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

Theorem alrimivv 1619
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 1618 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 1618 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1528
This theorem is referenced by:  2ax17  1622  euind  2953  sbnfc2  3142  uniintsn  3900  ssopab2dv  4292  ordelord  4413  suctr  4474  trsuc2OLD  4476  eusvnf  4528  ssrel  4775  relssdv  4778  eqrelrdv  4782  eqbrrdv  4783  eqrelrdv2  4785  ssrelrel  4786  iss  4997  funssres  5259  funun  5261  fununi  5281  fsn  5657  wemoiso  5816  wemoiso2  5817  oprabexd  5921  ovg  5947  omeu  6578  qliftfund  6739  eroveu  6748  th3qlem1  6759  fpwwe2lem11  8257  seqf1o  11081  summo  12184  pceu  12893  invfun  13660  psss  14317  spwmo  14329  gsumval3eu  15184  hausflimi  17669  vitalilem3  18959  plyexmo  19687  pjhthmo  21873  chscl  22212  cvmlift2lem12  23249  elfuns  23861  lineintmo  24187  isconcl5a  25500  isconcl5ab  25501  bosser  25566  trer  25626  unirep  25748  eqrelrdvOLD  26127  eqrelrdv2OLD  26128  prter1  26146  ismrcd2  26173  ismrc  26175  psgneu  26828  truniALT  27576  gen12  27658  sspwtrALT  27864  sspwtrALT2  27865  pwtrOLD  27867  pwtrrOLD  27869  suctrALT2  27881  trintALT  27925  suctrALTcf  27966  suctrALT3  27968  suctrALT4  27972  bnj1379  28130  bnj580  28212  bnj1321  28324  islpoldN  30941
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604
  Copyright terms: Public domain W3C validator