Theorem 19.21adv 1283

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

Syntax hints:   -> wi 3  A.wal 951

This theorem is referenced by:  zfpair 2767  ssrel 3237  funcnvuni 3550  eqfnfv 3782  cbvfo 3870  isofrlem 3886  f1oweALT 3891  tz7.49 3944  fodomfi 4540  aceq5lem4 4710  aceq5 4712  zorn2lem4 4763  zorn2lem7 4766  genpcl 5083  psslinpr 5107  prlem934 5111  ltaddpr 5112  ltexprlem3 5116  suplem1pr 5133  dfuz 6150  uzwo4OLD 6158  uzwo 6387  uzwoOLD 6388  metcnp4 7904

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

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

Copyright terms: Public domain