Theorem alrimivv 1936

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

Syntax hints:   → wi 4  ∀wal 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem is referenced by:  2ax5  1945  2mo  2649  euind  3626  sbnfc2  4337  uniintsn  4884  eusvnf  5270  ssopab2dv  5417  ssrel  5639  relssdv  5643  eqrelrdv  5647  eqbrrdv  5648  eqrelrdv2  5650  ssrelrel  5651  iss  5888  iresn0n0  5908  ordelord  6213  suctr  6274  funssres  6402  funun  6404  fununi  6433  fsn  6928  opabresex2d  7243  fvmptopab  7244  ovg  7351  wemoiso  7724  wemoiso2  7725  oprabexd  7726  frrlem9  8013  omeu  8291  qliftfund  8463  eroveu  8472  fpwwe2lem10  10219  addsrmo  10652  mulsrmo  10653  seqf1o  13582  fi1uzind  14028  brfi1indALT  14031  summo  15246  prodmo  15461  pceu  16362  invfun  17223  initoeu2lem2  17475  psss  18040  psgneu  18852  gsumval3eu  19243  hausflimi  22831  vitalilem3  24461  plyexmo  25160  tglineintmo  26687  frgr3vlem1  28310  3vfriswmgrlem  28314  frgr2wwlk1  28366  pjhthmo  29337  chscl  29676  bnj1379  32477  bnj580  32560  bnj1321  32674  acycgr1v  32778  cvmlift2lem12  32943  satffunlem1lem1  33031  satffunlem2lem1  33033  mclsssvlem  33191  mclsax  33198  mclsind  33199  nosupprefixmo  33589  noinfprefixmo  33590  nosupno  33592  noinfno  33607  lineintmo  34145  trer  34191  mbfresfi  35509  unirep  35557  iss2  36165  prter1  36579  islpoldN  39184  ismrcd2  40165  ismrc  40167  mnutrd  41512  truniALT  41775  gen12  41852  sspwtrALT  42056  sspwtrALT2  42057  suctrALT  42060  suctrALT2  42071  trintALT  42115  suctrALTcf  42156  suctrALT3  42158  rlimdmafv  44284  rlimdmafv2  44365  opabresex0d  44392  spr0nelg  44544  sprsymrelfvlem  44558  mofsn  45787  thincmo  45926