Theorem ifcli 4520

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

Syntax hints:   ∈ wcel 2111  ifcif 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4473

This theorem is referenced by:  ifex  4523  xaddf  13123  sadcf  16364  ramcl  16941  setcepi  17995  abvtrivd  20747  mvrf1  21923  mplcoe3  21973  psrbagsn  21998  evlslem1  22017  psdmplcl  22077  psdmul  22081  psdmvr  22084  marep01ma  22575  dscmet  24487  dscopn  24488  i1f1lem  25617  i1f1  25618  itg2const  25668  cxpval  26600  cxpcl  26610  recxpcl  26611  sqff1o  27119  chtublem  27149  dchrmullid  27190  bposlem1  27222  lgsval  27239  lgsfcl2  27241  lgscllem  27242  lgsval2lem  27245  lgsneg  27259  lgsdilem  27262  lgsdir2  27268  lgsdir  27270  lgsdi  27272  lgsne0  27273  dchrisum0flblem1  27446  dchrisum0flblem2  27447  dchrisum0fno1  27449  rpvmasum2  27450  omlsi  31384  indfval  32837  psgnfzto1stlem  33069  sgnsf  33131  ddemeas  34249  eulerpartlemb  34381  eulerpartlemgs2  34393  ex-sategoelel12  35471  sqdivzi  35772  poimirlem16  37686  poimirlem19  37689  pw2f1ocnv  43140  flcidc  43273  arearect  43318  sqrtcval  43744  sqrtcval2  43745  resqrtval  43746  imsqrtval  43747  limsup10exlem  45880  sqwvfourb  46337  fouriersw  46339  hspval  46717