Theorem alrimivv 1796

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

Syntax hints:   → wi 4  ∀wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1376  ax-gen 1378  ax-17 1459

This theorem is referenced by:  2ax17  1799  euind  2779  sbnfc2  2962  ssopab2dv  4033  suctr  4176  eusvnf  4203  ordsuc  4306  ssrel  4446  relssdv  4450  eqrelrdv  4454  eqbrrdv  4455  eqrelrdv2  4457  ssrelrel  4458  iss  4674  funssres  4962  funun  4964  fununi  4987  fsn  5356  ovg  5659  caovimo  5714  oprabexd  5774  qliftfund  6212  eroveu  6220  th3qlem1  6231  addnq0mo  6637  mulnq0mo  6638  ltexprlemdisj  6796  recexprlemdisj  6820  addsrmo  6920  mulsrmo  6921