Theorem keepel 4155

Description: Keep a membership hypothesis for weak deduction theorem, when special case B e. C is provable. (Contributed by NM, 14-Aug-1999.)

Hypotheses

Ref	Expression
keepel.1	|- A e. C
keepel.2	|- B e. C

Assertion

Ref	Expression
keepel	|- if ( ph , A , B ) e. C

Proof of Theorem keepel

Step	Hyp	Ref	Expression
1		eleq1 2689	. 2 |- ( A = if ( ph , A , B ) -> ( A e. C <-> if ( ph , A , B ) e. C ) )
2		eleq1 2689	. 2 |- ( B = if ( ph , A , B ) -> ( B e. C <-> if ( ph , A , B ) e. C ) )
3		keepel.1	. 2 |- A e. C
4		keepel.2	. 2 |- B e. C
5	1, 2, 3, 4	keephyp 4152	1 |- if ( ph , A , B ) e. C

Syntax hints:   e. wcel 1990   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  ifex  4156  xaddf  12055  sadcf  15175  ramcl  15733  setcepi  16738  abvtrivd  18840  mvrf1  19425  mplcoe3  19466  psrbagsn  19495  evlslem1  19515  marep01ma  20466  dscmet  22377  dscopn  22378  i1f1lem  23456  i1f1  23457  itg2const  23507  cxpval  24410  cxpcl  24420  recxpcl  24421  sqff1o  24908  chtublem  24936  dchrmulid2  24977  bposlem1  25009  lgsval  25026  lgsfcl2  25028  lgscllem  25029  lgsval2lem  25032  lgsneg  25046  lgsdilem  25049  lgsdir2  25055  lgsdir  25057  lgsdi  25059  lgsne0  25060  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0fno1  25200  rpvmasum2  25201  omlsi  28263  sgnsf  29729  psgnfzto1stlem  29850  indfval  30078  ddemeas  30299  eulerpartlemb  30430  eulerpartlemgs2  30442  sqdivzi  31610  poimirlem16  33425  poimirlem19  33428  pw2f1ocnv  37604  flcidc  37744  arearect  37801  ifcli  39329  sqwvfourb  40446  fouriersw  40448  hspval  40823