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

Theorem alrimivv 1622
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 1621 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 1621 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  2ax17  1630  euind  2965  sbnfc2  3154  uniintsn  3915  ssopab2dv  4309  ordelord  4430  suctr  4491  trsuc2OLD  4493  eusvnf  4545  ssrel  4792  relssdv  4795  eqrelrdv  4799  eqbrrdv  4800  eqrelrdv2  4802  ssrelrel  4803  iss  5014  funssres  5310  funun  5312  fununi  5332  fsn  5712  wemoiso  5871  wemoiso2  5872  oprabexd  5976  ovg  6002  omeu  6599  qliftfund  6760  eroveu  6769  th3qlem1  6780  fpwwe2lem11  8278  seqf1o  11103  summo  12206  pceu  12915  invfun  13682  psss  14339  spwmo  14351  gsumval3eu  15206  hausflimi  17691  vitalilem3  18981  plyexmo  19709  pjhthmo  21897  chscl  22236  cvmlift2lem12  23860  prodmo  24159  lineintmo  24852  isconcl5a  26204  isconcl5ab  26205  bosser  26270  trer  26330  unirep  26452  eqrelrdvOLD  26831  eqrelrdv2OLD  26832  prter1  26850  ismrcd2  26877  ismrc  26879  psgneu  27532  rlimdmafv  28145  frgra3vlem1  28424  3vfriswmgralem  28428  truniALT  28604  gen12  28695  sspwtrALT  28912  sspwtrALT2  28913  pwtrOLD  28915  pwtrrOLD  28917  suctrALT2  28929  trintALT  28973  suctrALTcf  29014  suctrALT3  29016  suctrALT4  29020  bnj1379  29179  bnj580  29261  bnj1321  29373  islpoldN  32296
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
  Copyright terms: Public domain W3C validator