Theorem ifcli 4571

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

Syntax hints:   ∈ wcel 2099  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-if 4525

This theorem is referenced by:  ifex  4574  xaddf  13227  sadcf  16419  ramcl  16989  setcepi  18068  abvtrivd  20709  mvrf1  21915  mplcoe3  21963  psrbagsn  21994  evlslem1  22015  psdmplcl  22073  psdmul  22077  marep01ma  22549  dscmet  24468  dscopn  24469  i1f1lem  25605  i1f1  25606  itg2const  25657  cxpval  26585  cxpcl  26595  recxpcl  26596  sqff1o  27101  chtublem  27131  dchrmullid  27172  bposlem1  27204  lgsval  27221  lgsfcl2  27223  lgscllem  27224  lgsval2lem  27227  lgsneg  27241  lgsdilem  27244  lgsdir2  27250  lgsdir  27252  lgsdi  27254  lgsne0  27255  dchrisum0flblem1  27428  dchrisum0flblem2  27429  dchrisum0fno1  27431  rpvmasum2  27432  omlsi  31201  psgnfzto1stlem  32799  sgnsf  32861  indfval  33571  ddemeas  33791  eulerpartlemb  33924  eulerpartlemgs2  33936  ex-sategoelel12  34973  sqdivzi  35258  poimirlem16  37044  poimirlem19  37047  pw2f1ocnv  42380  flcidc  42520  arearect  42566  sqrtcval  42994  sqrtcval2  42995  resqrtval  42996  imsqrtval  42997  limsup10exlem  45083  sqwvfourb  45540  fouriersw  45542  hspval  45920