Theorem alrimivv 1924

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (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 1923	. 2 ⊢ (𝜑 → ∀𝑦𝜓)
3	2	alrimiv 1923	1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1496  ax-gen 1498  ax-17 1575

This theorem is referenced by:  2ax17  1927  euind  3004  sbnfc2  3199  exmidsssn  4315  exmidel  4318  exmidundif  4319  exmidundifim  4320  ssopab2dv  4397  suctr  4542  eusvnf  4574  ordsuc  4685  ssrel  4838  relssdv  4842  eqrelrdv  4846  eqbrrdv  4847  eqrelrdv2  4849  ssrelrel  4850  iss  5084  funssres  5395  funun  5397  fununi  5424  fsn  5849  ovg  6193  caovimo  6248  oprabexd  6320  qliftfund  6852  eroveu  6860  th3qlem1  6871  exmidssfi  7199  exmidfodomrlemim  7504  exmidmotap  7575  addnq0mo  7762  mulnq0mo  7763  ltexprlemdisj  7921  recexprlemdisj  7945  addsrmo  8058  mulsrmo  8059  seqf1og  10883  summodc  12069  prodmodc  12264  pceu  12993  rhmex  14302  limcimo  15530  exmidsbth  16804  gfsumval  16862