Theorem alrimivv 1926

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

Syntax hints:   → wi 4  ∀wal 1535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem is referenced by:  2ax5  1935  2mo  2646  euind  3733  sbnfc2  4445  uniintsn  4990  eusvnf  5398  ssopab2dv  5561  ssrel  5795  ssrelOLD  5796  relssdv  5801  eqrelrdv  5805  eqbrrdv  5806  eqrelrdv2  5808  ssrelrel  5809  iss  6055  iresn0n0  6074  ordelord  6408  suctr  6472  funssres  6612  funun  6614  fununi  6643  fsn  7155  opabresex2d  7486  fvmptopabOLD  7488  ovg  7598  wemoiso  7997  wemoiso2  7998  oprabexd  7999  frrlem9  8318  omeu  8622  qliftfund  8842  eroveu  8851  fpwwe2lem10  10678  addsrmo  11111  mulsrmo  11112  seqf1o  14081  fi1uzind  14543  brfi1indALT  14546  summo  15750  prodmo  15969  pceu  16880  invfun  17812  initoeu2lem2  18069  psss  18638  psgneu  19539  gsumval3eu  19937  hausflimi  24004  vitalilem3  25659  plyexmo  26370  nosupprefixmo  27760  noinfprefixmo  27761  nosupno  27763  noinfno  27778  tglineintmo  28665  frgr3vlem1  30302  3vfriswmgrlem  30306  frgr2wwlk1  30358  pjhthmo  31331  chscl  31670  copsex2dv  32626  bnj1379  34823  bnj580  34906  bnj1321  35020  acycgr1v  35134  cvmlift2lem12  35299  satffunlem1lem1  35387  satffunlem2lem1  35389  mclsssvlem  35547  mclsax  35554  mclsind  35555  lineintmo  36139  trer  36299  mbfresfi  37653  unirep  37701  iss2  38326  prter1  38861  islpoldN  41467  ismrcd2  42687  ismrc  42689  tfsconcatb0  43334  mnutrd  44276  truniALT  44539  gen12  44616  sspwtrALT  44820  sspwtrALT2  44821  suctrALT  44824  suctrALT2  44835  trintALT  44879  suctrALTcf  44920  suctrALT3  44922  rlimdmafv  47127  rlimdmafv2  47208  opabresex0d  47235  spr0nelg  47401  sprsymrelfvlem  47415  mofsn  48674  thincmo  48829