Theorem ifcli 4578

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

Syntax hints:   ∈ wcel 2106  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  ifex  4581  xaddf  13263  sadcf  16487  ramcl  17063  setcepi  18142  abvtrivd  20850  mvrf1  22024  mplcoe3  22074  psrbagsn  22105  evlslem1  22124  psdmplcl  22184  psdmul  22188  marep01ma  22682  dscmet  24601  dscopn  24602  i1f1lem  25738  i1f1  25739  itg2const  25790  cxpval  26721  cxpcl  26731  recxpcl  26732  sqff1o  27240  chtublem  27270  dchrmullid  27311  bposlem1  27343  lgsval  27360  lgsfcl2  27362  lgscllem  27363  lgsval2lem  27366  lgsneg  27380  lgsdilem  27383  lgsdir2  27389  lgsdir  27391  lgsdi  27393  lgsne0  27394  dchrisum0flblem1  27567  dchrisum0flblem2  27568  dchrisum0fno1  27570  rpvmasum2  27571  omlsi  31433  psgnfzto1stlem  33103  sgnsf  33165  indfval  33997  ddemeas  34217  eulerpartlemb  34350  eulerpartlemgs2  34362  ex-sategoelel12  35412  sqdivzi  35708  poimirlem16  37623  poimirlem19  37626  pw2f1ocnv  43026  flcidc  43159  arearect  43204  sqrtcval  43631  sqrtcval2  43632  resqrtval  43633  imsqrtval  43634  limsup10exlem  45728  sqwvfourb  46185  fouriersw  46187  hspval  46565