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  2991  sbnfc2  3186  exmidsssn  4290  exmidel  4293  exmidundif  4294  exmidundifim  4295  ssopab2dv  4371  suctr  4516  eusvnf  4548  ordsuc  4659  ssrel  4812  relssdv  4816  eqrelrdv  4820  eqbrrdv  4821  eqrelrdv2  4823  ssrelrel  4824  iss  5057  funssres  5366  funun  5368  fununi  5395  fsn  5815  ovg  6156  caovimo  6211  oprabexd  6284  qliftfund  6782  eroveu  6790  th3qlem1  6801  exmidfodomrlemim  7402  exmidmotap  7470  addnq0mo  7657  mulnq0mo  7658  ltexprlemdisj  7816  recexprlemdisj  7840  addsrmo  7953  mulsrmo  7954  seqf1og  10773  summodc  11934  prodmodc  12129  pceu  12858  rhmex  14161  limcimo  15379  exmidsbth  16564