Theorem alrimivv 1923

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

Syntax hints:   → wi 4  ∀wal 1395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1495  ax-gen 1497  ax-17 1574

This theorem is referenced by:  2ax17  1926  euind  2993  sbnfc2  3188  exmidsssn  4292  exmidel  4295  exmidundif  4296  exmidundifim  4297  ssopab2dv  4373  suctr  4518  eusvnf  4550  ordsuc  4661  ssrel  4814  relssdv  4818  eqrelrdv  4822  eqbrrdv  4823  eqrelrdv2  4825  ssrelrel  4826  iss  5059  funssres  5369  funun  5371  fununi  5398  fsn  5819  ovg  6161  caovimo  6216  oprabexd  6289  qliftfund  6787  eroveu  6795  th3qlem1  6806  exmidssfi  7131  exmidfodomrlemim  7412  exmidmotap  7480  addnq0mo  7667  mulnq0mo  7668  ltexprlemdisj  7826  recexprlemdisj  7850  addsrmo  7963  mulsrmo  7964  seqf1og  10784  summodc  11962  prodmodc  12157  pceu  12886  rhmex  14190  limcimo  15408  exmidsbth  16679  gfsumval  16732