Theorem alrimivv 1855

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

Syntax hints:   → wi 4  ∀wal 1333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-5 1427  ax-gen 1429  ax-17 1506

This theorem is referenced by:  2ax17  1858  euind  2899  sbnfc2  3091  exmidsssn  4163  exmidel  4166  exmidundif  4167  exmidundifim  4168  ssopab2dv  4238  suctr  4381  eusvnf  4413  ordsuc  4522  ssrel  4674  relssdv  4678  eqrelrdv  4682  eqbrrdv  4683  eqrelrdv2  4685  ssrelrel  4686  iss  4912  funssres  5212  funun  5214  fununi  5238  fsn  5639  ovg  5959  caovimo  6014  oprabexd  6075  qliftfund  6563  eroveu  6571  th3qlem1  6582  exmidfodomrlemim  7136  addnq0mo  7367  mulnq0mo  7368  ltexprlemdisj  7526  recexprlemdisj  7550  addsrmo  7663  mulsrmo  7664  summodc  11280  prodmodc  11475  limcimo  13034  exmidsbth  13595