Theorem alrimivv 1886

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

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1458  ax-gen 1460  ax-17 1537

This theorem is referenced by:  2ax17  1889  euind  2939  sbnfc2  3132  exmidsssn  4217  exmidel  4220  exmidundif  4221  exmidundifim  4222  ssopab2dv  4293  suctr  4436  eusvnf  4468  ordsuc  4577  ssrel  4729  relssdv  4733  eqrelrdv  4737  eqbrrdv  4738  eqrelrdv2  4740  ssrelrel  4741  iss  4968  funssres  5273  funun  5275  fununi  5299  fsn  5704  ovg  6030  caovimo  6085  oprabexd  6146  qliftfund  6636  eroveu  6644  th3qlem1  6655  exmidfodomrlemim  7218  exmidmotap  7278  addnq0mo  7464  mulnq0mo  7465  ltexprlemdisj  7623  recexprlemdisj  7647  addsrmo  7760  mulsrmo  7761  summodc  11409  prodmodc  11604  pceu  12313  rhmex  13468  limcimo  14531  exmidsbth  15170