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

Theorem alrimivv 1920
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2198 and 19.21v 1931. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
alrimivv.1 (𝜑𝜓)
Assertion
Ref Expression
alrimivv (𝜑 → ∀𝑥𝑦𝜓)
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem alrimivv
StepHypRef Expression
1 alrimivv.1 . . 3 (𝜑𝜓)
21alrimiv 1919 . 2 (𝜑 → ∀𝑦𝜓)
32alrimiv 1919 1 (𝜑 → ∀𝑥𝑦𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem is referenced by:  2ax5  1929  2mo  2729  euind  3714  sbnfc2  4387  uniintsn  4906  eusvnf  5284  ssopab2dv  5430  ssrel  5651  relssdv  5655  eqrelrdv  5659  eqbrrdv  5660  eqrelrdv2  5662  ssrelrel  5663  iss  5897  iresn0n0  5917  ordelord  6207  suctr  6268  funssres  6392  funun  6394  fununi  6423  fsn  6890  opabresex2d  7197  fvmptopab  7198  ovg  7302  wemoiso  7665  wemoiso2  7666  oprabexd  7667  omeu  8201  qliftfund  8373  eroveu  8382  fpwwe2lem11  10051  addsrmo  10484  mulsrmo  10485  seqf1o  13401  fi1uzind  13845  brfi1indALT  13848  summo  15064  prodmo  15280  pceu  16173  invfun  17024  initoeu2lem2  17265  psss  17814  psgneu  18565  gsumval3eu  18955  hausflimi  22518  vitalilem3  24140  plyexmo  24831  tglineintmo  26356  frgr3vlem1  27980  3vfriswmgrlem  27984  frgr2wwlk1  28036  pjhthmo  29007  chscl  29346  bnj1379  32002  bnj580  32085  bnj1321  32197  acycgr1v  32294  cvmlift2lem12  32459  satffunlem1lem1  32547  satffunlem2lem1  32549  mclsssvlem  32707  mclsax  32714  mclsind  32715  frrlem9  33029  noprefixmo  33100  nosupno  33101  lineintmo  33516  trer  33562  mbfresfi  34820  unirep  34871  iss2  35484  prter1  35897  islpoldN  38502  ismrcd2  39176  ismrc  39178  mnutrd  40496  truniALT  40755  gen12  40832  sspwtrALT  41036  sspwtrALT2  41037  suctrALT  41040  suctrALT2  41051  trintALT  41095  suctrALTcf  41136  suctrALT3  41138  rlimdmafv  43257  rlimdmafv2  43338  opabresex0d  43365  spr0nelg  43485  sprsymrelfvlem  43499
  Copyright terms: Public domain W3C validator