Theorem alrimdv 1721

Description: Deduction form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1905 and 19.21v 1729. (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 1704	. 2
2		ax-5 1704	. 2
3		alrimdv.1	. 2
4	1, 2, 3	alrimdh 1672	1

Syntax hints:  ->wi 4  A.wal 1393

This theorem is referenced by:  axc9lem2  2040  zfpair  4689  fliftfun  6210  isofrlem  6236  funcnvuni  6753  f1oweALT  6784  findcard  7779  findcard2  7780  dfac5lem4  8528  dfac5  8530  zorn2lem4  8900  genpcl  9407  psslinpr  9430  ltaddpr  9433  ltexprlem3  9437  suplem1pr  9451  uzwo  11173  uzwoOLD  11174  seqf1o  12148  ramcl  14547  alexsubALTlem3  20549  truniALT  33312  ggen31  33317  onfrALTlem2  33318  gen21  33405  gen22  33408  ggen22  33409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1618  ax-4 1631  ax-5 1704