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  2924  sbnfc2  3117  exmidsssn  4200  exmidel  4203  exmidundif  4204  exmidundifim  4205  ssopab2dv  4276  suctr  4419  eusvnf  4451  ordsuc  4560  ssrel  4712  relssdv  4716  eqrelrdv  4720  eqbrrdv  4721  eqrelrdv2  4723  ssrelrel  4724  iss  4950  funssres  5255  funun  5257  fununi  5281  fsn  5685  ovg  6008  caovimo  6063  oprabexd  6123  qliftfund  6613  eroveu  6621  th3qlem1  6632  exmidfodomrlemim  7195  exmidmotap  7255  addnq0mo  7441  mulnq0mo  7442  ltexprlemdisj  7600  recexprlemdisj  7624  addsrmo  7737  mulsrmo  7738  summodc  11382  prodmodc  11577  pceu  12285  limcimo  13916  exmidsbth  14543