Theorem alrimivv 1889

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

Syntax hints:   → wi 4  ∀wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1461  ax-gen 1463  ax-17 1540

This theorem is referenced by:  2ax17  1892  euind  2951  sbnfc2  3145  exmidsssn  4235  exmidel  4238  exmidundif  4239  exmidundifim  4240  ssopab2dv  4313  suctr  4456  eusvnf  4488  ordsuc  4599  ssrel  4751  relssdv  4755  eqrelrdv  4759  eqbrrdv  4760  eqrelrdv2  4762  ssrelrel  4763  iss  4992  funssres  5300  funun  5302  fununi  5326  fsn  5734  ovg  6062  caovimo  6117  oprabexd  6184  qliftfund  6677  eroveu  6685  th3qlem1  6696  exmidfodomrlemim  7268  exmidmotap  7328  addnq0mo  7514  mulnq0mo  7515  ltexprlemdisj  7673  recexprlemdisj  7697  addsrmo  7810  mulsrmo  7811  seqf1og  10613  summodc  11548  prodmodc  11743  pceu  12464  rhmex  13713  limcimo  14901  exmidsbth  15668