Theorem alrimivv 1963

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1828  ax-4 1842  ax-5 1945

This theorem is used by:  2ax5  1972  2mo  2676  euind  3685  sbnfc2  4400  uniintsn  4948  eusvnf  5358  copsex2dv  5470  ssopab2dv  5530  ssrel  5764  relssdv  5769  eqrelrdv  5773  eqbrrdv  5774  eqrelrdv2  5776  ssrelrel  5777  iss  6038  iresn0n0  6057  ordelord  6399  suctr  6466  funssres  6601  funun  6603  fununi  6634  fsn  7157  ovg  7606  wemoiso  8006  wemoiso2  8007  oprabexd  8008  frrlem9  8337  omeu  8618  qliftfund  8849  eroveu  8858  fpwwe2lem10  10749  addsrmo  11182  mulsrmo  11183  seqf1o  14210  fi1uzind  14676  brfi1indALT  14679  summo  15909  prodmo  16129  pceu  17050  invfun  17965  initoeu2lem2  18216  psss  18780  psgneu  19747  gsumval3eu  20145  hausflimi  24326  vitalilem3  25958  plyexmo  26663  nosupprefixmo  28084  noinfprefixmo  28085  nosupno  28087  noinfno  28102  bdayons  28689  tglineintmo  29137  frgr3vlem1  30901  3vfriswmgrlem  30905  frgr2wwlk1  30957  pjhthmo  31931  chscl  32270  bnj1379  35527  bnj580  35610  bnj1321  35724  acycgr1v  36070  cvmlift2lem12  36245  satffunlem1lem1  36333  satffunlem2lem1  36335  mclsssvlem  36493  mclsax  36500  mclsind  36501  elpssmo  36635  lineintmo  37099  trer  37281  mbfresfi  38775  unirep  38839  iss2  39467  prter1  40127  islpoldN  42732  ismrcd2  43901  ismrc  43903  tfsconcatb0  44536  mnutrd  45454  truniALT  45713  gen12  45790  sspwtrALT  45993  sspwtrALT2  45994  suctrALT  45997  suctrALT2  46008  trintALT  46052  suctrALTcf  46093  suctrALT3  46095  rlimdmafv  48450  rlimdmafv2  48531  opabresex0d  48558  spr0nelg  48761  sprsymrelfvlem  48775  mofsn  50158  thincmo  50766  functhincfun  50787