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  4485  ordelord  4605  suctrALT  4666  suctr  4667  eusvnf  4720  ssrel  4966  relssdv  4970  eqrelrdv  4974  eqbrrdv  4975  eqrelrdv2  4977  ssrelrel  4978  iss  5191  funssres  5495  funun  5497  fununi  5519  fsn  5908  wemoiso  6080  wemoiso2  6081  oprabexd  6188  ovg  6214  omeu  6830  qliftfund  6992  eroveu  7001  th3qlem1  7012  fpwwe2lem11  8517  seqf1o  11366  brfi1uzind  11717  summo  12513  pceu  13222  invfun  13991  psss  14648  spwmo  14660  gsumval3eu  15515  hausflimi  18014  vitalilem3  19504  plyexmo  20232  pjhthmo  22806  chscl  23145  cvmlift2lem12  25003  prodmo  25264  lineintmo  26093  mbfresfi  26255  trer  26321  unirep  26416  prter1  26730  ismrcd2  26755  ismrc  26757  psgneu  27408  rlimdmafv  28019  frgra3vlem1  28392  3vfriswmgralem  28396  frg2wot1  28448  2spotdisj  28452  truniALT  28628  gen12  28721  sspwtrALT  28937  sspwtrALT2  28938  suctrALT2  28951  trintALT  28995  suctrALTcf  29036  suctrALT3  29038  bnj1379  29204  bnj580  29286  bnj1321  29398  islpoldN  32284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627
  Copyright terms: Public domain W3C validator