Theorem 19.22dv 1292

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

Syntax hints:   -> wi 3  E.wex 982

This theorem is referenced by:  19.22dvv 1294  immo 1419  moimv 1421  r19.22dv2 1739  cgsexg 1834  cla43egv 1869  ssel 2066  reupick 2282  uniss 2525  dmss 3316  funss 3540  funssres 3558  fv3 3739  dffo4 3826  dffo5 3827  fvclss 3861  cbvfo 3891  ecelqsi 4298  mapsn 4351  unfilem1 4560  ac6s 4766  cfub 4920  cflim 4921  nsmallpq 5095  ltexprlem1 5154  ltexprlem3 5156  ltexprlem4 5157  ltexpri 5161  prlem936 5167  reclem2pr 5169  reclem3pr 5170  suplem1pr 5173  suppsr2 5235  suppsr3 5236  supsrlem2 5238  pre-axsup 5303  xrsupsslem 6078  xrinfmsslem 6079  supxrre 6085  ivthlem7 7287  infxpidmlem10 7562  metelcls 7962  bcthlem8 8003  bcthlem14 8009  ubthlem6 8530  cnlnssadj 10008  homcardus 10526

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

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

Copyright terms: Public domain