Theorem alrimivv 1923

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

Syntax hints:   → wi 4  ∀wal 1529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1790  ax-4 1804  ax-5 1905

This theorem is referenced by:  2ax5  1932  2mo  2727  euind  3713  sbnfc2  4386  uniintsn  4904  eusvnf  5283  ssopab2dv  5429  ssrel  5650  relssdv  5654  eqrelrdv  5658  eqbrrdv  5659  eqrelrdv2  5661  ssrelrel  5662  iss  5896  iresn0n0  5916  ordelord  6206  suctr  6267  funssres  6391  funun  6393  fununi  6422  fsn  6890  opabresex2d  7200  fvmptopab  7201  ovg  7305  wemoiso  7666  wemoiso2  7667  oprabexd  7668  omeu  8203  qliftfund  8375  eroveu  8384  fpwwe2lem11  10054  addsrmo  10487  mulsrmo  10488  seqf1o  13403  fi1uzind  13847  brfi1indALT  13850  summo  15066  prodmo  15282  pceu  16175  invfun  17026  initoeu2lem2  17267  psss  17816  psgneu  18626  gsumval3eu  19016  hausflimi  22580  vitalilem3  24203  plyexmo  24894  tglineintmo  26420  frgr3vlem1  28044  3vfriswmgrlem  28048  frgr2wwlk1  28100  pjhthmo  29071  chscl  29410  bnj1379  32095  bnj580  32178  bnj1321  32292  acycgr1v  32389  cvmlift2lem12  32554  satffunlem1lem1  32642  satffunlem2lem1  32644  mclsssvlem  32802  mclsax  32809  mclsind  32810  frrlem9  33124  noprefixmo  33195  nosupno  33196  lineintmo  33611  trer  33657  mbfresfi  34930  unirep  34980  iss2  35593  prter1  36007  islpoldN  38612  ismrcd2  39287  ismrc  39289  mnutrd  40607  truniALT  40866  gen12  40943  sspwtrALT  41147  sspwtrALT2  41148  suctrALT  41151  suctrALT2  41162  trintALT  41206  suctrALTcf  41247  suctrALT3  41249  rlimdmafv  43367  rlimdmafv2  43448  opabresex0d  43475  spr0nelg  43629  sprsymrelfvlem  43643