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

Theorem alrimivv 1643
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 1642 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 1642 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550
This theorem is referenced by:  2ax17  1651  euind  3123  sbnfc2  3311  uniintsn  4089  ssopab2dv  4486  ordelord  4606  suctrALT  4667  suctr  4668  eusvnf  4721  ssrel  4967  relssdv  4971  eqrelrdv  4975  eqbrrdv  4976  eqrelrdv2  4978  ssrelrel  4979  iss  5192  funssres  5496  funun  5498  fununi  5520  fsn  5909  wemoiso  6081  wemoiso2  6082  oprabexd  6189  ovg  6215  omeu  6831  qliftfund  6993  eroveu  7002  th3qlem1  7013  fpwwe2lem11  8520  seqf1o  11369  brfi1uzind  11720  summo  12516  pceu  13225  invfun  13994  psss  14651  spwmo  14663  gsumval3eu  15518  hausflimi  18017  vitalilem3  19507  plyexmo  20235  pjhthmo  22809  chscl  23148  cvmlift2lem12  25006  prodmo  25267  lineintmo  26096  mbfresfi  26265  trer  26333  unirep  26428  prter1  26742  ismrcd2  26767  ismrc  26769  psgneu  27420  rlimdmafv  28031  frgra3vlem1  28464  3vfriswmgralem  28468  frg2wot1  28520  2spotdisj  28524  truniALT  28700  gen12  28793  sspwtrALT  29009  sspwtrALT2  29010  suctrALT2  29023  trintALT  29067  suctrALTcf  29108  suctrALT3  29110  bnj1379  29276  bnj580  29358  bnj1321  29470  islpoldN  32356
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1556  ax-5 1567  ax-17 1627
  Copyright terms: Public domain W3C validator