Theorem alrimivv 1804

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

Syntax hints:   → wi 4  ∀wal 1288

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-5 1382  ax-gen 1384  ax-17 1465

This theorem is referenced by:  2ax17  1807  euind  2803  sbnfc2  2989  exmidsssn  4040  exmidel  4042  exmidundif  4043  exmidundifim  4044  ssopab2dv  4114  suctr  4257  eusvnf  4288  ordsuc  4392  ssrel  4539  relssdv  4543  eqrelrdv  4547  eqbrrdv  4548  eqrelrdv2  4550  ssrelrel  4551  iss  4771  funssres  5069  funun  5071  fununi  5095  fsn  5483  ovg  5797  caovimo  5852  oprabexd  5912  qliftfund  6389  eroveu  6397  th3qlem1  6408  exmidfodomrlemim  6888  addnq0mo  7067  mulnq0mo  7068  ltexprlemdisj  7226  recexprlemdisj  7250  addsrmo  7350  mulsrmo  7351  isummo  10834  exmidsbth  12186