Theorem 19.20dv 1284

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

Syntax hints:   -> wi 3  A.wal 951

This theorem is referenced by:  19.20dvv 1286  moimv 1412  r19.20dv2 1703  mo2icl 1914  reuss2 2265  ssuni 2512  poss 2832  soss 2843  frss 2911  dfwe2 2925  ordom 3131  asymref2 3424  asymref2OLD 3426  funss 3520  eqfnfv 3782  dff2 3802  tz7.48lem 3940  abfii4 4538  zorn2lem4 4763  zorn2lem7 4766  suplem1pr 5133  suppsr2 5195  pre-axsup 5263  sup2 5998  metcnp4 7904  chsscm 9033  occont 9076

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

Copyright terms: Public domain