Theorem alrimdv 1678

Description: Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.)

Hypothesis

Ref	Expression
alrimdv.1

Assertion

Ref	Expression
alrimdv

Distinct variable groups:   ,   ,

Proof of Theorem alrimdv

Step	Hyp	Ref	Expression
1		ax-5 1661	. 2
2		ax-5 1661	. 2
3		alrimdv.1	. 2
4	1, 2, 3	alrimdh 1631	1

Syntax hints:  ->wi 4  A.wal 1580

This theorem is referenced by:  axc9lem2  1979  zfpair  4501  fliftfun  5973  isofrlem  5999  funcnvuni  6499  f1oweALT  6530  findcard  7510  findcard2  7511  dfac5lem4  8243  dfac5  8245  zorn2lem4  8615  genpcl  9123  psslinpr  9146  ltaddpr  9149  ltexprlem3  9153  suplem1pr  9167  uzwo  10862  uzwoOLD  10863  seqf1o  11788  ramcl  14030  alexsubALTlem3  19325  truniALT  30825  ggen31  30830  onfrALTlem2  30831  gen21  30919  gen22  30922  ggen22  30923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1586  ax-4 1597  ax-5 1661