Theorem 19.21adv 1286

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 969	. 2 |- (ph -> A.xph)
2		ax-17 969	. 2 |- (ps -> A.xps)
3		19.21adv.1	. 2 |- (ph -> (ps -> ch))
4	1, 2, 3	19.21ad 1057	1 |- (ph -> (ps -> A.xch))

Syntax hints:   -> wi 3  A.wal 952

This theorem is referenced by:  zfpair 2772  ssrel 3242  funcnvuni 3556  eqfnfv 3788  cbvfo 3876  isofrlem 3892  f1oweALT 3897  tz7.49 3950  fodomfi 4546  aceq5lem4 4718  aceq5 4720  zorn2lem4 4771  zorn2lem7 4774  genpcl 5091  psslinpr 5115  prlem934 5119  ltaddpr 5120  ltexprlem3 5124  suplem1pr 5141  dfuz 6158  uzwo4OLD 6166  uzwo 6395  uzwoOLD 6396  metcnp4 7920

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

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

Copyright terms: Public domain