Theorem alrimivv 1925

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

Syntax hints:   → wi 4  ∀wal 1531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem is referenced by:  2ax5  1934  2mo  2729  euind  3715  sbnfc2  4388  uniintsn  4906  eusvnf  5285  ssopab2dv  5431  ssrel  5652  relssdv  5656  eqrelrdv  5660  eqbrrdv  5661  eqrelrdv2  5663  ssrelrel  5664  iss  5898  iresn0n0  5918  ordelord  6208  suctr  6269  funssres  6393  funun  6395  fununi  6424  fsn  6892  opabresex2d  7202  fvmptopab  7203  ovg  7307  wemoiso  7668  wemoiso2  7669  oprabexd  7670  omeu  8205  qliftfund  8377  eroveu  8386  fpwwe2lem11  10056  addsrmo  10489  mulsrmo  10490  seqf1o  13405  fi1uzind  13849  brfi1indALT  13852  summo  15068  prodmo  15284  pceu  16177  invfun  17028  initoeu2lem2  17269  psss  17818  psgneu  18628  gsumval3eu  19018  hausflimi  22582  vitalilem3  24205  plyexmo  24896  tglineintmo  26422  frgr3vlem1  28046  3vfriswmgrlem  28050  frgr2wwlk1  28102  pjhthmo  29073  chscl  29412  bnj1379  32097  bnj580  32180  bnj1321  32294  acycgr1v  32391  cvmlift2lem12  32556  satffunlem1lem1  32644  satffunlem2lem1  32646  mclsssvlem  32804  mclsax  32811  mclsind  32812  frrlem9  33126  noprefixmo  33197  nosupno  33198  lineintmo  33613  trer  33659  mbfresfi  34932  unirep  34982  iss2  35595  prter1  36009  islpoldN  38614  ismrcd2  39289  ismrc  39291  mnutrd  40609  truniALT  40868  gen12  40945  sspwtrALT  41149  sspwtrALT2  41150  suctrALT  41153  suctrALT2  41164  trintALT  41208  suctrALTcf  41249  suctrALT3  41251  rlimdmafv  43369  rlimdmafv2  43450  opabresex0d  43477  spr0nelg  43631  sprsymrelfvlem  43645