Theorem keepel 3030

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

Syntax hints:   e. wcel 1300  ifcif 2982

This theorem is referenced by:  ifex 3031  divmulzi 6895  divclzi 6900  divcan1zi 6907  divcan2zi 6908  recne0zi 6914  divreczi 6921  divdirzi 6932  divcan3zi 6936  rec11i 6954  redivclzi 6977  prodgt0i 6997  ltmul1i 7000  ltdiv1i 7002  ltreci 7062  discrlem2 7907  sqrlem21 7943  sqrlem22 7944  sqrthi 7949  sqrcli 7950  sqrgt0i 7951  sqrmuli 7955  abslem2 8161  dscmet 9196  projlem7 10825  omlsi 10879  osumlem8 11220

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-if 2983

Copyright terms: Public domain