Theorem alrimivv 1875

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

Syntax hints:   → wi 4  ∀wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1447  ax-gen 1449  ax-17 1526

This theorem is referenced by:  2ax17  1878  euind  2925  sbnfc2  3118  exmidsssn  4203  exmidel  4206  exmidundif  4207  exmidundifim  4208  ssopab2dv  4279  suctr  4422  eusvnf  4454  ordsuc  4563  ssrel  4715  relssdv  4719  eqrelrdv  4723  eqbrrdv  4724  eqrelrdv2  4726  ssrelrel  4727  iss  4954  funssres  5259  funun  5261  fununi  5285  fsn  5689  ovg  6013  caovimo  6068  oprabexd  6128  qliftfund  6618  eroveu  6626  th3qlem1  6637  exmidfodomrlemim  7200  exmidmotap  7260  addnq0mo  7446  mulnq0mo  7447  ltexprlemdisj  7605  recexprlemdisj  7629  addsrmo  7742  mulsrmo  7743  summodc  11391  prodmodc  11586  pceu  12295  limcimo  14137  exmidsbth  14775