Theorem alrimivv 1957

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1824  ax-4 1838  ax-5 1939

This theorem is used by:  2ax5  1966  2mo  2675  euind  3686  sbnfc2  4403  uniintsn  4949  eusvnf  5362  copsex2dv  5476  ssopab2dv  5535  ssrel  5768  relssdv  5773  eqrelrdv  5777  eqbrrdv  5778  eqrelrdv2  5780  ssrelrel  5781  iss  6036  iresn0n0  6055  ordelord  6382  suctr  6449  funssres  6580  funun  6582  fununi  6611  fsn  7131  ovg  7577  wemoiso  7968  wemoiso2  7969  oprabexd  7970  frrlem9  8289  omeu  8568  qliftfund  8799  eroveu  8808  fpwwe2lem10  10631  addsrmo  11064  mulsrmo  11065  seqf1o  14086  fi1uzind  14551  brfi1indALT  14554  summo  15775  prodmo  15997  pceu  16912  invfun  17827  initoeu2lem2  18078  psss  18642  psgneu  19582  gsumval3eu  19980  hausflimi  24148  vitalilem3  25780  plyexmo  26485  nosupprefixmo  27875  noinfprefixmo  27876  nosupno  27878  noinfno  27893  bdayons  28480  tglineintmo  28926  frgr3vlem1  30635  3vfriswmgrlem  30639  frgr2wwlk1  30691  pjhthmo  31665  chscl  32004  bnj1379  35227  bnj580  35310  bnj1321  35424  acycgr1v  35649  cvmlift2lem12  35814  satffunlem1lem1  35902  satffunlem2lem1  35904  mclsssvlem  36062  mclsax  36069  mclsind  36070  lineintmo  36657  trer  36855  mbfresfi  38345  unirep  38393  iss2  39021  prter1  39681  islpoldN  42286  ismrcd2  43458  ismrc  43460  tfsconcatb0  44099  mnutrd  45018  truniALT  45278  gen12  45355  sspwtrALT  45558  sspwtrALT2  45559  suctrALT  45562  suctrALT2  45573  trintALT  45617  suctrALTcf  45658  suctrALT3  45660  rlimdmafv  47942  rlimdmafv2  48023  opabresex0d  48050  spr0nelg  48253  sprsymrelfvlem  48267  mofsn  49650  thincmo  50234  functhincfun  50255