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

Theorem alrimivv 1778
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1992 and 19.21v 1790. (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 1777 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 1777 1  |-  ( ph  ->  A. x A. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1673  ax-4 1686  ax-5 1762
This theorem is referenced by:  2ax5  1788  2mo  2381  euind  3193  sbnfc2  3764  uniintsn  4242  eusvnf  4571  ssopab2dv  4703  ssrel  4901  relssdv  4905  eqrelrdv  4909  eqbrrdv  4910  eqrelrdv2  4912  ssrelrel  4913  iss  5130  ordelord  5424  suctr  5485  funssres  5601  funun  5603  fununi  5631  fsn  6046  ovg  6423  wemoiso  6766  wemoiso2  6767  oprabexd  6768  omeu  7273  qliftfund  7436  eroveu  7445  fpwwe2lem11  9052  addsrmo  9484  mulsrmo  9485  seqf1o  12248  fi1uzind  12645  brfi1indALT  12648  summo  13794  prodmo  14001  pceu  14807  invfun  15680  initoeu2lem2  15921  psss  16471  psgneu  17158  gsumval3eu  17549  hausflimi  21006  vitalilem3  22580  plyexmo  23278  tglineintmo  24699  frgra3vlem1  25740  3vfriswmgralem  25744  frg2wot1  25797  2spotdisj  25801  pjhthmo  26967  chscl  27306  bnj1379  29648  bnj580  29730  bnj1321  29842  cvmlift2lem12  30043  mclsssvlem  30206  mclsax  30213  mclsind  30214  lineintmo  30930  trer  30978  mbfresfi  31989  unirep  32041  prter1  32453  islpoldN  35054  ismrcd2  35543  ismrc  35545  truniALT  36903  gen12  36997  sspwtrALT  37207  sspwtrALT2  37216  suctrALT  37219  suctrALT2  37230  trintALT  37275  suctrALTcf  37316  suctrALT3  37318  rlimdmafv  38770  opabresex0d  39123  opabresex2d  39127
  Copyright terms: Public domain W3C validator