Theorem alrimivv 1950

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

Syntax hints:   → wi 4  ∀wal 1560

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

This theorem is referenced by:  2ax5  1959  2mo  2677  euind  3689  sbnfc2  4395  uniintsn  4945  eusvnf  5351  copsex2dv  5465  ssopab2dv  5524  ssrel  5757  relssdv  5762  eqrelrdv  5766  eqbrrdv  5767  eqrelrdv2  5769  ssrelrel  5770  iss  6026  iresn0n0  6045  ordelord  6370  suctr  6436  funssres  6567  funun  6569  fununi  6598  fsn  7119  ovg  7563  wemoiso  7956  wemoiso2  7957  oprabexd  7958  frrlem9  8277  omeu  8556  qliftfund  8787  eroveu  8796  fpwwe2lem10  10600  addsrmo  11033  mulsrmo  11034  seqf1o  14058  fi1uzind  14522  brfi1indALT  14525  summo  15746  prodmo  15968  pceu  16884  invfun  17799  initoeu2lem2  18050  psss  18614  psgneu  19548  gsumval3eu  19946  hausflimi  24042  vitalilem3  25674  plyexmo  26379  nosupprefixmo  27766  noinfprefixmo  27767  nosupno  27769  noinfno  27784  bdayons  28371  tglineintmo  28813  frgr3vlem1  30477  3vfriswmgrlem  30481  frgr2wwlk1  30533  pjhthmo  31507  chscl  31846  bnj1379  35127  bnj580  35210  bnj1321  35324  acycgr1v  35504  cvmlift2lem12  35669  satffunlem1lem1  35757  satffunlem2lem1  35759  mclsssvlem  35917  mclsax  35924  mclsind  35925  lineintmo  36512  trer  36681  mbfresfi  38170  unirep  38218  iss2  38848  prter1  39508  islpoldN  42113  ismrcd2  43285  ismrc  43287  tfsconcatb0  43926  mnutrd  44861  truniALT  45122  gen12  45199  sspwtrALT  45402  sspwtrALT2  45403  suctrALT  45406  suctrALT2  45417  trintALT  45461  suctrALTcf  45502  suctrALT3  45504  rlimdmafv  47776  rlimdmafv2  47857  opabresex0d  47884  spr0nelg  48087  sprsymrelfvlem  48101  mofsn  49470  thincmo  50054  functhincfun  50075