Theorem 19.20dv 1291

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:   ph,x

Proof of Theorem 19.20dv

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

Syntax hints:   -> wi 3  A.wal 956

This theorem is referenced by:  19.20dvv 1293  moimv 1421  r19.20dv2 1714  mo2icl 1926  reuss2 2279  ssuni 2527  poss 2848  soss 2859  frss 2928  dfwe2 2942  ordom 3148  asymref2 3447  funss 3541  eqfnfv 3804  dff2 3824  tz7.48lem 3962  zorn2lem4 4808  zorn2lem7 4811  suplem1pr 5180  suppsr2 5242  pre-axsup 5310  sup2 6060  metcnp4 7974  chsscm 9114  occont 9162

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

Copyright terms: Public domain