Theorem alrimivv 1632

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)

Hypothesis

Ref	Expression
alrimivv.1	|- (ph -> ps)

Assertion

Ref	Expression
alrimivv	|- (ph -> A.xA.yps)

Distinct variable groups:   ph,x   ph,y

Allowed substitution hints:   ps(x,y)

Proof of Theorem alrimivv

Step	Hyp	Ref	Expression
1		alrimivv.1	. . 3 |- (ph -> ps)
2	1	alrimiv 1631	. 2 |- (ph -> A.yps)
3	2	alrimiv 1631	1 |- (ph -> A.xA.yps)

Syntax hints:   -> wi 4  A.wal 1540

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

This theorem is referenced by:  2ax17  1640  euind  3024  sbnfc2  3197  uniintsn  3964  eqrelkrdv  4215  nnsucelr  4429  ssfin  4471  ssopab2dv  4716  ssrel  4845  relssdv  4850  eqrelrdv  4853  eqoprrdv  4855  funun  5147  fununi  5161  funsi  5521  ovg  5602  fntxp  5805  fnpprod  5844  fundmen  6044  enpw1  6063  enmap2lem4  6067  enmap1lem4  6073  enprmaplem3  6079  fnfrec  6321