Theorem 19.20dv 1287

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

Syntax hints:   -> wi 3  A.wal 952

This theorem is referenced by:  19.20dvv 1289  moimv 1417  r19.20dv2 1708  mo2icl 1919  reuss2 2271  ssuni 2517  poss 2836  soss 2847  frss 2916  dfwe2 2930  ordom 3136  asymref2 3432  funss 3526  eqfnfv 3788  dff2 3808  tz7.48lem 3946  abfii4 4544  zorn2lem4 4771  zorn2lem7 4774  suplem1pr 5141  suppsr2 5203  pre-axsup 5271  sup2 6006  metcnp4 7920  chsscm 9051  occont 9099

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

Copyright terms: Public domain