Theorem 19.22dv 1285

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

Syntax hints:   -> wi 3  E.wex 977

This theorem is referenced by:  19.22dvv 1287  immo 1410  moimv 1412  r19.22dv2 1728  cgsexg 1822  cla43egv 1857  ssel 2053  reupick 2269  uniss 2511  nnsuc 3138  dmss 3299  funss 3520  funssres 3538  fv3 3718  dffo4 3805  dffo5 3806  fvclss 3840  cbvfo 3870  ecelqsi 4276  mapsn 4329  ssnn 4514  unfilem1 4524  ac6s 4728  zorn2lem7 4766  alephval3 4875  cfub 4880  cflim 4881  nsmallpq 5055  ltexprlem1 5114  ltexprlem3 5116  ltexprlem4 5117  ltexpri 5121  prlem936 5127  reclem2pr 5129  reclem3pr 5130  suplem1pr 5133  suppsr2 5195  suppsr3 5196  supsrlem2 5198  pre-axsup 5263  xrsupsslem 6023  xrinfmsslem 6024  supxrre 6030  ivthlem7 7222  ivthlem7OLD 7231  infxpidmlem10 7504  metelcls 7900  bcthlem8 7940  bcthlem14 7946  ubthlem6 8465  shless 9262  cnlnssadj 9928

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

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

Copyright terms: Public domain