Theorem alrimivv 1928

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

Syntax hints:   → wi 4  ∀wal 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem is referenced by:  2ax5  1937  2mo  2641  euind  3692  sbnfc2  4398  uniintsn  4945  eusvnf  5342  copsex2dv  5449  ssopab2dv  5506  ssrel  5737  relssdv  5742  eqrelrdv  5746  eqbrrdv  5747  eqrelrdv2  5749  ssrelrel  5750  iss  5995  iresn0n0  6014  ordelord  6342  suctr  6408  funssres  6544  funun  6546  fununi  6575  fsn  7089  ovg  7534  wemoiso  7931  wemoiso2  7932  oprabexd  7933  frrlem9  8250  omeu  8526  qliftfund  8753  eroveu  8762  fpwwe2lem10  10569  addsrmo  11002  mulsrmo  11003  seqf1o  13984  fi1uzind  14448  brfi1indALT  14451  summo  15659  prodmo  15878  pceu  16793  invfun  17706  initoeu2lem2  17957  psss  18521  psgneu  19420  gsumval3eu  19818  hausflimi  23900  vitalilem3  25544  plyexmo  26254  nosupprefixmo  27645  noinfprefixmo  27646  nosupno  27648  noinfno  27663  bdayon  28213  tglineintmo  28622  frgr3vlem1  30252  3vfriswmgrlem  30256  frgr2wwlk1  30308  pjhthmo  31281  chscl  31620  bnj1379  34813  bnj580  34896  bnj1321  35010  acycgr1v  35129  cvmlift2lem12  35294  satffunlem1lem1  35382  satffunlem2lem1  35384  mclsssvlem  35542  mclsax  35549  mclsind  35550  lineintmo  36138  trer  36297  mbfresfi  37653  unirep  37701  iss2  38319  prter1  38865  islpoldN  41471  ismrcd2  42680  ismrc  42682  tfsconcatb0  43326  mnutrd  44262  truniALT  44524  gen12  44601  sspwtrALT  44804  sspwtrALT2  44805  suctrALT  44808  suctrALT2  44819  trintALT  44863  suctrALTcf  44904  suctrALT3  44906  rlimdmafv  47171  rlimdmafv2  47252  opabresex0d  47279  spr0nelg  47470  sprsymrelfvlem  47484  mofsn  48825  thincmo  49410  functhincfun  49431