Theorem alrimivv 1875

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

Syntax hints:   → wi 4  ∀wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1447  ax-gen 1449  ax-17 1526

This theorem is referenced by:  2ax17  1878  euind  2926  sbnfc2  3119  exmidsssn  4204  exmidel  4207  exmidundif  4208  exmidundifim  4209  ssopab2dv  4280  suctr  4423  eusvnf  4455  ordsuc  4564  ssrel  4716  relssdv  4720  eqrelrdv  4724  eqbrrdv  4725  eqrelrdv2  4727  ssrelrel  4728  iss  4955  funssres  5260  funun  5262  fununi  5286  fsn  5690  ovg  6015  caovimo  6070  oprabexd  6130  qliftfund  6620  eroveu  6628  th3qlem1  6639  exmidfodomrlemim  7202  exmidmotap  7262  addnq0mo  7448  mulnq0mo  7449  ltexprlemdisj  7607  recexprlemdisj  7631  addsrmo  7744  mulsrmo  7745  summodc  11393  prodmodc  11588  pceu  12297  limcimo  14173  exmidsbth  14811