Theorem alrimivv 1843

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

Syntax hints:   → wi 4  ∀wal 1473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem is referenced by:  2ax5  1853  2mo  2539  euind  3360  sbnfc2  3959  uniintsn  4449  eusvnf  4787  ssopab2dv  4929  ssrel  5130  ssrelOLD  5131  relssdv  5135  eqrelrdv  5139  eqbrrdv  5140  eqrelrdv2  5142  ssrelrel  5143  iss  5367  ordelord  5662  suctr  5725  suctrOLD  5726  funssres  5844  funun  5846  fununi  5878  fsn  6308  ovg  6697  wemoiso  7044  wemoiso2  7045  oprabexd  7046  omeu  7552  qliftfund  7720  eroveu  7729  fpwwe2lem11  9341  addsrmo  9773  mulsrmo  9774  seqf1o  12704  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  summo  14295  prodmo  14505  pceu  15389  invfun  16247  initoeu2lem2  16488  psss  17037  psgneu  17749  gsumval3eu  18128  hausflimi  21594  vitalilem3  23185  plyexmo  23872  tglineintmo  25337  frgra3vlem1  26527  3vfriswmgralem  26531  frg2wot1  26584  2spotdisj  26588  pjhthmo  27545  chscl  27884  bnj1379  30155  bnj580  30237  bnj1321  30349  cvmlift2lem12  30550  mclsssvlem  30713  mclsax  30720  mclsind  30721  lineintmo  31434  trer  31480  mbfresfi  32626  unirep  32677  prter1  33182  islpoldN  35791  ismrcd2  36280  ismrc  36282  truniALT  37772  gen12  37864  sspwtrALT  38071  sspwtrALT2  38080  suctrALT  38083  suctrALT2  38094  trintALT  38139  suctrALTcf  38180  suctrALT3  38182  rlimdmafv  39906  opabresex0d  40330  opabresex2d  40334  frgr3vlem1  41443  3vfriswmgrlem  41447  frgr2wwlk1  41494