Theorem ifcli 4525

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

Syntax hints:   ∈ wcel 2113  ifcif 4477

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-if 4478

This theorem is referenced by:  ifex  4528  xaddf  13137  sadcf  16378  ramcl  16955  setcepi  18010  abvtrivd  20763  mvrf1  21939  mplcoe3  21991  psrbagsn  22016  evlslem1  22035  psdmplcl  22103  psdmul  22107  psdmvr  22110  marep01ma  22602  dscmet  24514  dscopn  24515  i1f1lem  25644  i1f1  25645  itg2const  25695  cxpval  26627  cxpcl  26637  recxpcl  26638  sqff1o  27146  chtublem  27176  dchrmullid  27217  bposlem1  27249  lgsval  27266  lgsfcl2  27268  lgscllem  27269  lgsval2lem  27272  lgsneg  27286  lgsdilem  27289  lgsdir2  27295  lgsdir  27297  lgsdi  27299  lgsne0  27300  dchrisum0flblem1  27473  dchrisum0flblem2  27474  dchrisum0fno1  27476  rpvmasum2  27477  omlsi  31428  indfval  32884  psgnfzto1stlem  33131  sgnsf  33193  ddemeas  34342  eulerpartlemb  34474  eulerpartlemgs2  34486  ex-sategoelel12  35570  sqdivzi  35871  poimirlem16  37776  poimirlem19  37779  pw2f1ocnv  43221  flcidc  43354  arearect  43399  sqrtcval  43824  sqrtcval2  43825  resqrtval  43826  imsqrtval  43827  limsup10exlem  45958  sqwvfourb  46415  fouriersw  46417  hspval  46795