Theorem ifcli 4575

Description: Inference associated with ifcl 4573. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4586 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 4573	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
4	1, 2, 3	mp2an 690	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 2106  ifcif 4528

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-if 4529

This theorem is referenced by:  ifex  4578  xaddf  13202  sadcf  16393  ramcl  16961  setcepi  18037  abvtrivd  20447  mvrf1  21544  mplcoe3  21592  psrbagsn  21623  evlslem1  21644  marep01ma  22161  dscmet  24080  dscopn  24081  i1f1lem  25205  i1f1  25206  itg2const  25257  cxpval  26171  cxpcl  26181  recxpcl  26182  sqff1o  26683  chtublem  26711  dchrmullid  26752  bposlem1  26784  lgsval  26801  lgsfcl2  26803  lgscllem  26804  lgsval2lem  26807  lgsneg  26821  lgsdilem  26824  lgsdir2  26830  lgsdir  26832  lgsdi  26834  lgsne0  26835  dchrisum0flblem1  27008  dchrisum0flblem2  27009  dchrisum0fno1  27011  rpvmasum2  27012  omlsi  30652  psgnfzto1stlem  32254  sgnsf  32316  indfval  33009  ddemeas  33229  eulerpartlemb  33362  eulerpartlemgs2  33374  ex-sategoelel12  34413  sqdivzi  34692  poimirlem16  36499  poimirlem19  36502  pw2f1ocnv  41766  flcidc  41906  arearect  41954  sqrtcval  42382  sqrtcval2  42383  resqrtval  42384  imsqrtval  42385  limsup10exlem  44478  sqwvfourb  44935  fouriersw  44937  hspval  45315