Theorem alrimivv 1930

Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2215 and 19.21v 1941. (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 1929	. 2 ⊢ (𝜑 → ∀𝑦𝜓)
3	2	alrimiv 1929	1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem is referenced by:  2ax5  1939  2mo  2649  euind  3684  sbnfc2  4393  uniintsn  4942  eusvnf  5341  copsex2dv  5452  ssopab2dv  5509  ssrel  5742  relssdv  5747  eqrelrdv  5751  eqbrrdv  5752  eqrelrdv2  5754  ssrelrel  5755  iss  6004  iresn0n0  6023  ordelord  6349  suctr  6415  funssres  6546  funun  6548  fununi  6577  fsn  7092  ovg  7535  wemoiso  7929  wemoiso2  7930  oprabexd  7931  frrlem9  8248  omeu  8524  qliftfund  8754  eroveu  8763  fpwwe2lem10  10565  addsrmo  10998  mulsrmo  10999  seqf1o  13980  fi1uzind  14444  brfi1indALT  14447  summo  15654  prodmo  15873  pceu  16788  invfun  17702  initoeu2lem2  17953  psss  18517  psgneu  19452  gsumval3eu  19850  hausflimi  23941  vitalilem3  25584  plyexmo  26294  nosupprefixmo  27685  noinfprefixmo  27686  nosupno  27688  noinfno  27703  bdayons  28289  tglineintmo  28732  frgr3vlem1  30366  3vfriswmgrlem  30370  frgr2wwlk1  30422  pjhthmo  31396  chscl  31735  bnj1379  35012  bnj580  35095  bnj1321  35209  acycgr1v  35371  cvmlift2lem12  35536  satffunlem1lem1  35624  satffunlem2lem1  35626  mclsssvlem  35784  mclsax  35791  mclsind  35792  lineintmo  36379  trer  36538  mbfresfi  37946  unirep  37994  iss2  38624  prter1  39284  islpoldN  41889  ismrcd2  43085  ismrc  43087  tfsconcatb0  43730  mnutrd  44665  truniALT  44926  gen12  45003  sspwtrALT  45206  sspwtrALT2  45207  suctrALT  45210  suctrALT2  45221  trintALT  45265  suctrALTcf  45306  suctrALT3  45308  rlimdmafv  47566  rlimdmafv2  47647  opabresex0d  47674  spr0nelg  47865  sprsymrelfvlem  47879  mofsn  49232  thincmo  49816  functhincfun  49837