Theorem alrimivv 1921

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

Syntax hints:   → wi 4  ∀wal 1393

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

This theorem is referenced by:  2ax17  1924  euind  2990  sbnfc2  3185  exmidsssn  4286  exmidel  4289  exmidundif  4290  exmidundifim  4291  ssopab2dv  4367  suctr  4512  eusvnf  4544  ordsuc  4655  ssrel  4807  relssdv  4811  eqrelrdv  4815  eqbrrdv  4816  eqrelrdv2  4818  ssrelrel  4819  iss  5051  funssres  5360  funun  5362  fununi  5389  fsn  5807  ovg  6144  caovimo  6199  oprabexd  6272  qliftfund  6765  eroveu  6773  th3qlem1  6784  exmidfodomrlemim  7379  exmidmotap  7447  addnq0mo  7634  mulnq0mo  7635  ltexprlemdisj  7793  recexprlemdisj  7817  addsrmo  7930  mulsrmo  7931  seqf1og  10743  summodc  11894  prodmodc  12089  pceu  12818  rhmex  14121  limcimo  15339  exmidsbth  16392