Theorem 19.20dv 1289

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 971	. 2 |- (ph -> A.xph)
2		19.20dv.1	. 2 |- (ph -> (ps -> ch))
3	1, 2	19.20d 996	1 |- (ph -> (A.xps -> A.xch))

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  19.20dvv 1291  moimv 1419  r19.20dv2 1711  mo2icl 1923  reuss2 2275  ssuni 2522  poss 2841  soss 2852  frss 2921  dfwe2 2935  ordom 3141  asymref2 3440  funss 3534  eqfnfv 3797  dff2 3817  tz7.48lem 3955  abfii4OLD 4564  zorn2lem4 4791  zorn2lem7 4794  suplem1pr 5161  suppsr2 5223  pre-axsup 5291  sup2 6051  metcnp4 7970  chsscm 9112  occont 9160

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

Copyright terms: Public domain