Theorem alrimivv 1848

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

Syntax hints:   → wi 4  ∀wal 1330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1424  ax-gen 1426  ax-17 1507

This theorem is referenced by:  2ax17  1851  euind  2875  sbnfc2  3065  exmidsssn  4133  exmidel  4136  exmidundif  4137  exmidundifim  4138  ssopab2dv  4208  suctr  4351  eusvnf  4382  ordsuc  4486  ssrel  4635  relssdv  4639  eqrelrdv  4643  eqbrrdv  4644  eqrelrdv2  4646  ssrelrel  4647  iss  4873  funssres  5173  funun  5175  fununi  5199  fsn  5600  ovg  5917  caovimo  5972  oprabexd  6033  qliftfund  6520  eroveu  6528  th3qlem1  6539  exmidfodomrlemim  7074  addnq0mo  7279  mulnq0mo  7280  ltexprlemdisj  7438  recexprlemdisj  7462  addsrmo  7575  mulsrmo  7576  summodc  11184  prodmodc  11379  limcimo  12842  exmidsbth  13394