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  5809  ovg  6150  caovimo  6205  oprabexd  6278  qliftfund  6773  eroveu  6781  th3qlem1  6792  exmidfodomrlemim  7390  exmidmotap  7458  addnq0mo  7645  mulnq0mo  7646  ltexprlemdisj  7804  recexprlemdisj  7828  addsrmo  7941  mulsrmo  7942  seqf1og  10755  summodc  11910  prodmodc  12105  pceu  12834  rhmex  14137  limcimo  15355  exmidsbth  16480