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  4236  exmidel  4239  exmidundif  4240  exmidundifim  4241  ssopab2dv  4314  suctr  4457  eusvnf  4489  ordsuc  4600  ssrel  4752  relssdv  4756  eqrelrdv  4760  eqbrrdv  4761  eqrelrdv2  4763  ssrelrel  4764  iss  4993  funssres  5301  funun  5303  fununi  5327  fsn  5737  ovg  6066  caovimo  6121  oprabexd  6193  qliftfund  6686  eroveu  6694  th3qlem1  6705  exmidfodomrlemim  7282  exmidmotap  7346  addnq0mo  7533  mulnq0mo  7534  ltexprlemdisj  7692  recexprlemdisj  7716  addsrmo  7829  mulsrmo  7830  seqf1og  10632  summodc  11567  prodmodc  11762  pceu  12491  rhmex  13791  limcimo  15009  exmidsbth  15781