Theorem ifcli 4514

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

Syntax hints:   ∈ wcel 2114  ifcif 4466

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  ifex  4517  indfval  12166  xaddf  13176  sadcf  16422  ramcl  17000  setcepi  18055  abvtrivd  20809  mvrf1  21964  mplcoe3  22016  psrbagsn  22041  evlslem1  22060  psdmplcl  22128  psdmul  22132  psdmvr  22135  marep01ma  22625  dscmet  24537  dscopn  24538  i1f1lem  25656  i1f1  25657  itg2const  25707  cxpval  26628  cxpcl  26638  recxpcl  26639  sqff1o  27145  chtublem  27174  dchrmullid  27215  bposlem1  27247  lgsval  27264  lgsfcl2  27266  lgscllem  27267  lgsval2lem  27270  lgsneg  27284  lgsdilem  27287  lgsdir2  27293  lgsdir  27295  lgsdi  27297  lgsne0  27298  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0fno1  27474  rpvmasum2  27475  omlsi  31475  psgnfzto1stlem  33161  sgnsf  33223  ddemeas  34380  eulerpartlemb  34512  eulerpartlemgs2  34524  ex-sategoelel12  35609  sqdivzi  35910  poimirlem16  37957  poimirlem19  37960  pw2f1ocnv  43465  flcidc  43598  arearect  43643  sqrtcval  44068  sqrtcval2  44069  resqrtval  44070  imsqrtval  44071  limsup10exlem  46200  sqwvfourb  46657  fouriersw  46659  hspval  47037