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  26998  gen12  27080  sspwtrALT  27286  sspwtrALT2  27287  pwtrOLD  27289  pwtrrOLD  27291  suctrALT2  27303  trintALT  27347  suctrALTcf  27388  suctrALT3  27390  suctrALT4  27394  bnj1379  27552  bnj580  27634  bnj1321  27746  islpoldN  30363
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