Theorem alrimivv 1927

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem is referenced by:  2ax5  1936  2mo  2651  euind  3746  sbnfc2  4462  uniintsn  5009  eusvnf  5410  ssopab2dv  5570  ssrel  5806  ssrelOLD  5807  relssdv  5812  eqrelrdv  5816  eqbrrdv  5817  eqrelrdv2  5819  ssrelrel  5820  iss  6064  iresn0n0  6083  ordelord  6417  suctr  6481  funssres  6622  funun  6624  fununi  6653  fsn  7169  opabresex2d  7503  fvmptopabOLD  7505  ovg  7615  wemoiso  8014  wemoiso2  8015  oprabexd  8016  frrlem9  8335  omeu  8641  qliftfund  8861  eroveu  8870  fpwwe2lem10  10709  addsrmo  11142  mulsrmo  11143  seqf1o  14094  fi1uzind  14556  brfi1indALT  14559  summo  15765  prodmo  15984  pceu  16893  invfun  17825  initoeu2lem2  18082  psss  18650  psgneu  19548  gsumval3eu  19946  hausflimi  24009  vitalilem3  25664  plyexmo  26373  nosupprefixmo  27763  noinfprefixmo  27764  nosupno  27766  noinfno  27781  tglineintmo  28668  frgr3vlem1  30305  3vfriswmgrlem  30309  frgr2wwlk1  30361  pjhthmo  31334  chscl  31673  copsex2dv  32628  bnj1379  34806  bnj580  34889  bnj1321  35003  acycgr1v  35117  cvmlift2lem12  35282  satffunlem1lem1  35370  satffunlem2lem1  35372  mclsssvlem  35530  mclsax  35537  mclsind  35538  lineintmo  36121  trer  36282  mbfresfi  37626  unirep  37674  iss2  38300  prter1  38835  islpoldN  41441  ismrcd2  42655  ismrc  42657  tfsconcatb0  43306  mnutrd  44249  truniALT  44512  gen12  44589  sspwtrALT  44793  sspwtrALT2  44794  suctrALT  44797  suctrALT2  44808  trintALT  44852  suctrALTcf  44893  suctrALT3  44895  rlimdmafv  47092  rlimdmafv2  47173  opabresex0d  47200  spr0nelg  47350  sprsymrelfvlem  47364  mofsn  48557  thincmo  48696