Theorem keepel 2370

Description: Keep a membership hypothesis for weak deduction theorem, when special case B e. C is provable.

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 1510	. 2 |- (A = if(ph, A, B) -> (A e. C <-> if(ph, A, B) e. C))
2		eleq1 1510	. 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 2367	1 |- if(ph, A, B) e. C

Syntax hints:   e. wcel 1105  ifcif 2332

This theorem is referenced by:  ifex 2371  divmulz 5626  divclz 5631  divcan1z 5638  divcan2z 5639  recne0z 5645  divrecz 5652  divdirz 5663  divcan3z 5667  rec11 5685  redivclz 5706  prodgt0 5726  ltmul1 5729  ltdiv1 5731  ltrec 5778  discrlem2 6538  sqrlem21 6574  sqrlem22 6575  sqrth 6580  sqrcl 6581  sqrgt0 6582  sqrmul 6586  abslem2 6797  dscmet 7804  projlem7 9322  omls 9375  osumlem8 9716

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-if 2333

Copyright terms: Public domain