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  7554  exmidmotap  7628  addnq0mo  7815  mulnq0mo  7816  ltexprlemdisj  7974  recexprlemdisj  7998  addsrmo  8111  mulsrmo  8112  seqf1og  10973  summodc  12169  prodmodc  12364  pceu  13097  gsumvalfi  14236  rhmex  14548  limcimo  15857  wexmiddiffi  17210  exmidsbth  17235