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

Theorem alrimivv 1618
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 1617 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 1617 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527
This theorem is referenced by:  2ax17  1621  euind  2952  sbnfc2  3141  uniintsn  3899  ssopab2dv  4293  ordelord  4414  suctr  4475  trsuc2OLD  4477  eusvnf  4529  ssrel  4776  relssdv  4779  eqrelrdv  4783  eqbrrdv  4784  eqrelrdv2  4786  ssrelrel  4787  iss  4998  funssres  5294  funun  5296  fununi  5316  fsn  5696  wemoiso  5855  wemoiso2  5856  oprabexd  5960  ovg  5986  omeu  6583  qliftfund  6744  eroveu  6753  th3qlem1  6764  fpwwe2lem11  8262  seqf1o  11087  summo  12190  pceu  12899  invfun  13666  psss  14323  spwmo  14335  gsumval3eu  15190  hausflimi  17675  vitalilem3  18965  plyexmo  19693  pjhthmo  21881  chscl  22220  cvmlift2lem12  23845  lineintmo  24780  isconcl5a  26101  isconcl5ab  26102  bosser  26167  trer  26227  unirep  26349  eqrelrdvOLD  26728  eqrelrdv2OLD  26729  prter1  26747  ismrcd2  26774  ismrc  26776  psgneu  27429  frgra3vlem1  28178  3vfriswmgralem  28182  truniALT  28305  gen12  28390  sspwtrALT  28596  sspwtrALT2  28597  pwtrOLD  28599  pwtrrOLD  28601  suctrALT2  28613  trintALT  28657  suctrALTcf  28698  suctrALT3  28700  suctrALT4  28704  bnj1379  28863  bnj580  28945  bnj1321  29057  islpoldN  31674
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
  Copyright terms: Public domain W3C validator