Theorem 19.22dv 1290

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

Syntax hints:   -> wi 3  E.wex 980

This theorem is referenced by:  19.22dvv 1292  immo 1417  moimv 1419  r19.22dv2 1736  cgsexg 1831  cla43egv 1866  ssel 2063  reupick 2279  uniss 2521  dmss 3310  funss 3534  funssres 3552  fv3 3733  dffo4 3820  dffo5 3821  fvclss 3855  cbvfo 3885  ecelqsi 4292  mapsn 4345  unfilem1 4548  ac6s 4756  cfub 4908  cflim 4909  nsmallpq 5083  ltexprlem1 5142  ltexprlem3 5144  ltexprlem4 5145  ltexpri 5149  prlem936 5155  reclem2pr 5157  reclem3pr 5158  suplem1pr 5161  suppsr2 5223  suppsr3 5224  supsrlem2 5226  pre-axsup 5291  xrsupsslem 6076  xrinfmsslem 6077  supxrre 6083  ivthlem7 7287  infxpidmlem10 7561  metelcls 7965  bcthlem8 8006  bcthlem14 8012  ubthlem6 8534  cnlnssadj 10013  homcardus 10540

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

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

Copyright terms: Public domain