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

Theorem alrimivv 2014
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 2013 . 2  |-  ( ph  ->  A. y ps )
32alrimiv 2013 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  2017  euind  2920  sbnfc2  3102  uniintsn  3859  ssopab2dv  4251  ordelord  4372  suctr  4433  trsuc2OLD  4435  eusvnf  4487  ssrel  4750  relssdv  4753  eqrelrdv  4757  eqbrrdv  4758  eqrelrdv2  4760  ssrelrel  4761  iss  4972  funssres  5218  funun  5220  fununi  5240  fsn  5616  wemoiso  5775  wemoiso2  5776  oprabexd  5880  ovg  5906  omeu  6537  qliftfund  6698  eroveu  6707  th3qlem1  6718  fpwwe2lem11  8216  seqf1o  11039  summo  12141  pceu  12847  invfun  13614  psss  14271  spwmo  14283  gsumval3eu  15138  hausflimi  17623  vitalilem3  18913  plyexmo  19641  pjhthmo  21827  chscl  22184  cvmlift2lem12  23203  elfuns  23815  lineintmo  24141  isconcl5a  25454  isconcl5ab  25455  bosser  25520  trer  25580  unirep  25702  eqrelrdvOLD  26081  eqrelrdv2OLD  26082  prter1  26100  ismrcd2  26127  ismrc  26129  psgneu  26782  truniALT  27342  gen12  27424  sspwtrALT  27630  sspwtrALT2  27631  pwtrOLD  27633  pwtrrOLD  27635  suctrALT2  27647  trintALT  27691  suctrALTcf  27732  suctrALT3  27734  suctrALT4  27738  bnj1379  27896  bnj580  27978  bnj1321  28090  islpoldN  30825
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