Theorem alrimivv 1898

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

Syntax hints:   → wi 4  ∀wal 1371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1470  ax-gen 1472  ax-17 1549

This theorem is referenced by:  2ax17  1901  euind  2960  sbnfc2  3154  exmidsssn  4246  exmidel  4249  exmidundif  4250  exmidundifim  4251  ssopab2dv  4325  suctr  4468  eusvnf  4500  ordsuc  4611  ssrel  4763  relssdv  4767  eqrelrdv  4771  eqbrrdv  4772  eqrelrdv2  4774  ssrelrel  4775  iss  5005  funssres  5313  funun  5315  fununi  5342  fsn  5752  ovg  6085  caovimo  6140  oprabexd  6212  qliftfund  6705  eroveu  6713  th3qlem1  6724  exmidfodomrlemim  7309  exmidmotap  7373  addnq0mo  7560  mulnq0mo  7561  ltexprlemdisj  7719  recexprlemdisj  7743  addsrmo  7856  mulsrmo  7857  seqf1og  10666  summodc  11694  prodmodc  11889  pceu  12618  rhmex  13919  limcimo  15137  exmidsbth  15963