Theorem 19.22dv 1288

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

Hypothesis

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

Assertion

Ref	Expression
19.22dv	|- (ph -> (E.xps -> E.xch))

Distinct variable group:   ph,x

Proof of Theorem 19.22dv

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

Syntax hints:   -> wi 3  E.wex 978

This theorem is referenced by:  19.22dvv 1290  immo 1415  moimv 1417  r19.22dv2 1733  cgsexg 1827  cla43egv 1862  ssel 2059  reupick 2275  uniss 2516  nnsuc 3143  dmss 3305  funss 3526  funssres 3544  fv3 3724  dffo4 3811  dffo5 3812  fvclss 3846  cbvfo 3876  ecelqsi 4282  mapsn 4335  ssnn 4520  unfilem1 4530  ac6s 4736  zorn2lem7 4774  alephval3 4883  cfub 4888  cflim 4889  nsmallpq 5063  ltexprlem1 5122  ltexprlem3 5124  ltexprlem4 5125  ltexpri 5129  prlem936 5135  reclem2pr 5137  reclem3pr 5138  suplem1pr 5141  suppsr2 5203  suppsr3 5204  supsrlem2 5206  pre-axsup 5271  xrsupsslem 6031  xrinfmsslem 6032  supxrre 6038  ivthlem7 7230  ivthlem7OLD 7239  infxpidmlem10 7512  metelcls 7916  bcthlem8 7956  bcthlem14 7962  ubthlem6 8478  shless 9285  cnlnssadj 9951

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979

Copyright terms: Public domain