Theorem alrimivv 1955

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2249 and 19.21v 1966. (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

Step	Hyp	Ref	Expression
1		alrimivv.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	alrimiv 1954	. 2 ⊢ (𝜑 → ∀𝑦𝜓)
3	2	alrimiv 1954	1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem is referenced by:  2ax5  1964  2mo  2682  euind  3694  sbnfc2  4408  uniintsn  4952  eusvnf  5364  copsex2dv  5478  ssopab2dv  5537  ssrel  5770  relssdv  5775  eqrelrdv  5779  eqbrrdv  5780  eqrelrdv2  5782  ssrelrel  5783  iss  6038  iresn0n0  6057  ordelord  6383  suctr  6450  funssres  6581  funun  6583  fununi  6612  fsn  7132  ovg  7576  wemoiso  7970  wemoiso2  7971  oprabexd  7972  frrlem9  8291  omeu  8570  qliftfund  8801  eroveu  8810  fpwwe2lem10  10625  addsrmo  11058  mulsrmo  11059  seqf1o  14079  fi1uzind  14544  brfi1indALT  14547  summo  15768  prodmo  15990  pceu  16906  invfun  17821  initoeu2lem2  18072  psss  18636  psgneu  19576  gsumval3eu  19974  hausflimi  24106  vitalilem3  25738  plyexmo  26443  nosupprefixmo  27830  noinfprefixmo  27831  nosupno  27833  noinfno  27848  bdayons  28435  tglineintmo  28877  frgr3vlem1  30565  3vfriswmgrlem  30569  frgr2wwlk1  30621  pjhthmo  31595  chscl  31934  bnj1379  35163  bnj580  35246  bnj1321  35360  acycgr1v  35574  cvmlift2lem12  35739  satffunlem1lem1  35827  satffunlem2lem1  35829  mclsssvlem  35987  mclsax  35994  mclsind  35995  lineintmo  36582  trer  36750  mbfresfi  38240  unirep  38288  iss2  38918  prter1  39578  islpoldN  42183  ismrcd2  43357  ismrc  43359  tfsconcatb0  43998  mnutrd  44917  truniALT  45177  gen12  45254  sspwtrALT  45457  sspwtrALT2  45458  suctrALT  45461  suctrALT2  45472  trintALT  45516  suctrALTcf  45557  suctrALT3  45559  rlimdmafv  47838  rlimdmafv2  47919  opabresex0d  47946  spr0nelg  48149  sprsymrelfvlem  48163  mofsn  49542  thincmo  50126  functhincfun  50147