Theorem 19.20dv 946

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

Hypothesis

Ref	Expression
19.20dv.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
19.20dv	|- (ph -> (A.xps -> A.xch))

Distinct variable group(s):   ph,x

Proof of Theorem 19.20dv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.xph)
2		19.20dv.1	. 2 |- (ph -> (ps -> ch))
3	1, 2	19.20d 693	1 |- (ph -> (A.xps -> A.xch))

Syntax hints:   -> wi 2  A.wal 672

This theorem is referenced by:  19.20dvv 948  moimv 1044  mo2icl 1434  ssuni 1937  poss 2129  soss 2140  frss 2173  dfwe2 2187  ordom 2382  funss 2682  cleqfv 2880  tz7.48lem 2993  zornlem4 3606  zornlem7 3609  suplem1pr 3955  suppsr2 4017  axsup 4088  sup2 4510  chsscm 5147  occont 5168

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

metamath.org