Theorem keepel 1796

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

Syntax hints:   e. wcel 1092  ifcif 1776

This theorem is referenced by:  ifex 1797  divmulz 4219  divclz 4222  divcan1z 4226  divcan2z 4227  recneq0z 4232  divrecz 4237  divdistrz 4245  divcan3z 4249  rec11 4262  redivclz 4275  recgt0 4386  prodgt0 4388  divgt0 4390  divge0 4392  ltmul1 4394  ltdiv 4399  ltrec 4410  ltdiv23 4413  discrlem2 4714  sqrlem21 4751  sqrlem22 4752  sqrth 4757  sqrcl 4758  sqrgt0 4759  sqrmul 4763  abslem2 4867  climuni 4884  hlimcau 5142  hlimuni 5144  projlem7 5199  omls 5251  osumlem8 5537

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-if 1777

metamath.org