Theorem alrimivv 1928

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 1927	. 2 ⊢ (𝜑 → ∀𝑦𝜓)
3	2	alrimiv 1927	1 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)

Syntax hints:   → wi 4  ∀wal 1400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1500  ax-gen 1502  ax-17 1579

This theorem is referenced by:  2ax17  1931  euind  3013  sbnfc2  3208  exmidsssn  4334  exmidel  4337  exmidundif  4338  exmidundifim  4339  ssopab2dv  4416  suctr  4561  eusvnf  4594  ordsuc  4705  ssrel  4858  relssdv  4862  eqrelrdv  4866  eqbrrdv  4867  eqrelrdv2  4869  ssrelrel  4870  iss  5104  funssres  5415  funun  5417  fununi  5444  fsn  5871  ovg  6218  caovimo  6273  oprabexd  6350  qliftfund  6882  eroveu  6890  th3qlem1  6901  exmidssfi  7236  exmidfodomrlemim  7543  exmidmotap  7617  addnq0mo  7804  mulnq0mo  7805  ltexprlemdisj  7963  recexprlemdisj  7987  addsrmo  8100  mulsrmo  8101  seqf1og  10936  summodc  12128  prodmodc  12323  pceu  13052  gsumvalfi  14129  rhmex  14437  limcimo  15689  exmidsbth  16974