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 ⊢ (𝜑 → ∀𝑥∀𝑦𝜓)

This proof depends on syntax axioms:   → wi 4  ∀wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1500  ax-gen 1502  ax-17 1579

This theorem is used by:  2ax17  1931  euind  3013  sbnfc2  3208  exmidsssn  4339  exmidel  4342  exmidundif  4343  exmidundifim  4344  ssopab2dv  4421  suctr  4566  eusvnf  4599  ordsuc  4710  ssrel  4863  relssdv  4867  eqrelrdv  4871  eqbrrdv  4872  eqrelrdv2  4874  ssrelrel  4875  iss  5109  funssres  5420  funun  5422  fununi  5449  fsn  5880  ovg  6228  caovimo  6283  oprabexd  6360  qliftfund  6892  eroveu  6900  th3qlem1  6911  exmidssfi  7246  exmidfodomrlemim  7553  exmidmotap  7627  addnq0mo  7814  mulnq0mo  7815  ltexprlemdisj  7973  recexprlemdisj  7997  addsrmo  8110  mulsrmo  8111  seqf1og  10958  summodc  12150  prodmodc  12345  pceu  13074  gsumvalfi  14152  rhmex  14464  limcimo  15766  wexmiddiffi  17044  exmidsbth  17069