Theorem alrimivv 1899

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

Syntax hints:   → wi 4  ∀wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1471  ax-gen 1473  ax-17 1550

This theorem is referenced by:  2ax17  1902  euind  2967  sbnfc2  3162  exmidsssn  4262  exmidel  4265  exmidundif  4266  exmidundifim  4267  ssopab2dv  4343  suctr  4486  eusvnf  4518  ordsuc  4629  ssrel  4781  relssdv  4785  eqrelrdv  4789  eqbrrdv  4790  eqrelrdv2  4792  ssrelrel  4793  iss  5024  funssres  5332  funun  5334  fununi  5361  fsn  5775  ovg  6108  caovimo  6163  oprabexd  6235  qliftfund  6728  eroveu  6736  th3qlem1  6747  exmidfodomrlemim  7340  exmidmotap  7408  addnq0mo  7595  mulnq0mo  7596  ltexprlemdisj  7754  recexprlemdisj  7778  addsrmo  7891  mulsrmo  7892  seqf1og  10703  summodc  11809  prodmodc  12004  pceu  12733  rhmex  14034  limcimo  15252  exmidsbth  16165