Theorem ifcli 4576

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

Syntax hints:   ∈ wcel 2098  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-if 4530

This theorem is referenced by:  ifex  4579  xaddf  13235  sadcf  16427  ramcl  16997  setcepi  18076  abvtrivd  20724  mvrf1  21935  mplcoe3  21983  psrbagsn  22014  evlslem1  22035  psdmplcl  22094  psdmul  22098  marep01ma  22592  dscmet  24511  dscopn  24512  i1f1lem  25648  i1f1  25649  itg2const  25700  cxpval  26628  cxpcl  26638  recxpcl  26639  sqff1o  27144  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  31270  psgnfzto1stlem  32878  sgnsf  32940  indfval  33705  ddemeas  33925  eulerpartlemb  34058  eulerpartlemgs2  34070  ex-sategoelel12  35107  sqdivzi  35392  poimirlem16  37179  poimirlem19  37182  pw2f1ocnv  42523  flcidc  42663  arearect  42708  sqrtcval  43136  sqrtcval2  43137  resqrtval  43138  imsqrtval  43139  limsup10exlem  45223  sqwvfourb  45680  fouriersw  45682  hspval  46060