Theorem ifcli 4506

Description: Inference associated with ifcl 4504. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4517 when the special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 14-Aug-1999.) (Proof shortened by BJ, 1-Sep-2022.)

Hypotheses

Ref	Expression
ifcli.1	⊢ 𝐴 ∈ 𝐶
ifcli.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
ifcli	⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶

Proof of Theorem ifcli

Step	Hyp	Ref	Expression
1		ifcli.1	. 2 ⊢ 𝐴 ∈ 𝐶
2		ifcli.2	. 2 ⊢ 𝐵 ∈ 𝐶
3		ifcl 4504	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
4	1, 2, 3	mp2an 689	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 2106  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-if 4460

This theorem is referenced by:  ifex  4509  xaddf  12958  sadcf  16160  ramcl  16730  setcepi  17803  abvtrivd  20100  mvrf1  21194  mplcoe3  21239  psrbagsn  21271  evlslem1  21292  marep01ma  21809  dscmet  23728  dscopn  23729  i1f1lem  24853  i1f1  24854  itg2const  24905  cxpval  25819  cxpcl  25829  recxpcl  25830  sqff1o  26331  chtublem  26359  dchrmulid2  26400  bposlem1  26432  lgsval  26449  lgsfcl2  26451  lgscllem  26452  lgsval2lem  26455  lgsneg  26469  lgsdilem  26472  lgsdir2  26478  lgsdir  26480  lgsdi  26482  lgsne0  26483  dchrisum0flblem1  26656  dchrisum0flblem2  26657  dchrisum0fno1  26659  rpvmasum2  26660  omlsi  29766  psgnfzto1stlem  31367  sgnsf  31429  indfval  31984  ddemeas  32204  eulerpartlemb  32335  eulerpartlemgs2  32347  ex-sategoelel12  33389  sqdivzi  33693  poimirlem16  35793  poimirlem19  35796  pw2f1ocnv  40859  flcidc  40999  arearect  41046  sqrtcval  41249  sqrtcval2  41250  resqrtval  41251  imsqrtval  41252  limsup10exlem  43313  sqwvfourb  43770  fouriersw  43772  hspval  44147