Theorem 19.21adv 1288

Description: Deduction from Theorem 19.21 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.21adv.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
19.21adv	|- (ph -> (ps -> A.xch))

Distinct variable groups:   ph,x   ps,x

Proof of Theorem 19.21adv

Step	Hyp	Ref	Expression
1		ax-17 971	. 2 |- (ph -> A.xph)
2		ax-17 971	. 2 |- (ps -> A.xps)
3		19.21adv.1	. 2 |- (ph -> (ps -> ch))
4	1, 2, 3	19.21ad 1059	1 |- (ph -> (ps -> A.xch))

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  zfpair 2777  ssrel 3247  funcnvuni 3564  eqfnfv 3797  cbvfo 3885  isofrlem 3901  f1oweALT 3906  tz7.49 3959  fodomfiOLD 4566  aceq5lem4 4738  aceq5 4740  zorn2lem4 4791  zorn2lem7 4794  genpcl 5111  psslinpr 5135  prlem934 5139  ltaddpr 5140  ltexprlem3 5144  suplem1pr 5161  dfuz 6202  uzwo4OLD 6210  uzwo 6455  uzwoOLD 6456  metcnp4 7970

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain