Theorem alrimivv 1923

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

Syntax hints:   → wi 4  ∀wal 1396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1496  ax-gen 1498  ax-17 1575

This theorem is referenced by:  2ax17  1926  euind  2994  sbnfc2  3189  exmidsssn  4298  exmidel  4301  exmidundif  4302  exmidundifim  4303  ssopab2dv  4379  suctr  4524  eusvnf  4556  ordsuc  4667  ssrel  4820  relssdv  4824  eqrelrdv  4828  eqbrrdv  4829  eqrelrdv2  4831  ssrelrel  4832  iss  5065  funssres  5376  funun  5378  fununi  5405  fsn  5827  ovg  6171  caovimo  6226  oprabexd  6298  qliftfund  6830  eroveu  6838  th3qlem1  6849  exmidssfi  7174  exmidfodomrlemim  7472  exmidmotap  7540  addnq0mo  7727  mulnq0mo  7728  ltexprlemdisj  7886  recexprlemdisj  7910  addsrmo  8023  mulsrmo  8024  seqf1og  10846  summodc  12024  prodmodc  12219  pceu  12948  rhmex  14252  limcimo  15476  exmidsbth  16752  gfsumval  16809