Theorem 19.21adv 945

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 group(s):   ph,x   ps,x

Proof of Theorem 19.21adv

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

Syntax hints:   -> wi 2  A.wal 672

This theorem is referenced by:  zfpair 1891  relss 2480  funcnvuni 2706  cleqfv 2880  cbvfo 2923  isofrlem 2939  f1oweOLD 2944  tz7.49 2997  aceq5lem4 3561  aceq5 3563  zornlem4 3606  zornlem7 3609  genpcl 3905  psslinpr 3929  prlem934 3933  ltaddpr 3934  ltexprlem3 3938  suplem1pr 3955  uzwo 4605  nnwoOLD 4608

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org