Theorem alrimivv 1632

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	⊢ (φ → ∀x∀yψ)

Distinct variable groups:   φ,x   φ,y

Allowed substitution hints:   ψ(x,y)

Proof of Theorem alrimivv

Step	Hyp	Ref	Expression
1		alrimivv.1	. . 3 ⊢ (φ → ψ)
2	1	alrimiv 1631	. 2 ⊢ (φ → ∀yψ)
3	2	alrimiv 1631	1 ⊢ (φ → ∀x∀yψ)

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616

This theorem is referenced by:  2ax17  1640  euind  3023  sbnfc2  3196  uniintsn  3963  eqrelkrdv  4214  nnsucelr  4428  ssfin  4470  ssopab2dv  4715  ssrel  4844  relssdv  4849  eqrelrdv  4852  eqoprrdv  4854  funun  5146  fununi  5160  funsi  5520  ovg  5601  fntxp  5804  fnpprod  5843  fundmen  6043  enpw1  6062  enmap2lem4  6066  enmap1lem4  6072  enprmaplem3  6078  fnfrec  6320