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

Theorem alrimivv 2013
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 2012 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 2012 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6   A.wal 1532
This theorem is referenced by:  2ax17  2016  euind  2889  sbnfc2  3069  uniintsn  3797  ssopab2dv  4186  ordelord  4307  suctr  4368  trsuc2OLD  4370  eusvnf  4420  ssrel  4683  relssdv  4686  eqrelrdv  4690  eqbrrdv  4691  eqrelrdv2  4693  ssrelrel  4694  iss  4905  funssres  5151  funun  5153  fununi  5173  fsn  5548  wemoiso  5707  wemoiso2  5708  oprabexd  5812  ovg  5838  omeu  6469  qliftfund  6630  eroveu  6639  th3qlem1  6650  supmo  7087  fpwwe2lem11  8142  seqf1o  10965  sqrmo  11614  summo  12067  pceu  12773  invfun  13510  psss  14158  spwmo  14170  gsumval3eu  15025  hausflimi  17507  vitalilem3  18797  plyexmo  19525  pjhthmo  21711  chscl  22068  cvmlift2lem12  23016  elfuns  23628  lineintmo  23954  isconcl5a  25267  isconcl5ab  25268  bosser  25333  trer  25393  unirep  25515  eqrelrdvOLD  25894  eqrelrdv2OLD  25895  prter1  25913  ismrcd2  25940  ismrc  25942  psgneu  26595  truniALT  27095  gen12  27177  sspwtrALT  27383  sspwtrALT2  27384  pwtrOLD  27386  pwtrrOLD  27388  suctrALT2  27400  trintALT  27444  suctrALTcf  27485  suctrALT3  27487  suctrALT4  27491  bnj1379  27649  bnj580  27731  bnj1321  27843  islpoldN  30578
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540
  Copyright terms: Public domain W3C validator