Theorem ifcli 4390

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

Syntax hints:   ∈ wcel 2050  ifcif 4344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-if 4345

This theorem is referenced by:  ifex  4392  xaddf  12432  sadcf  15660  ramcl  16219  setcepi  17218  abvtrivd  19345  mvrf1  19931  mplcoe3  19972  psrbagsn  20000  evlslem1  20020  marep01ma  20985  dscmet  22897  dscopn  22898  i1f1lem  24005  i1f1  24006  itg2const  24056  cxpval  24960  cxpcl  24970  recxpcl  24971  sqff1o  25473  chtublem  25501  dchrmulid2  25542  bposlem1  25574  lgsval  25591  lgsfcl2  25593  lgscllem  25594  lgsval2lem  25597  lgsneg  25611  lgsdilem  25614  lgsdir2  25620  lgsdir  25622  lgsdi  25624  lgsne0  25625  dchrisum0flblem1  25798  dchrisum0flblem2  25799  dchrisum0fno1  25801  rpvmasum2  25802  omlsi  28974  sgnsf  30499  psgnfzto1stlem  30720  indfval  30948  ddemeas  31169  eulerpartlemb  31300  eulerpartlemgs2  31312  sqdivzi  32508  poimirlem16  34378  poimirlem19  34381  pw2f1ocnv  39059  flcidc  39199  arearect  39247  limsup10exlem  41509  sqwvfourb  41970  fouriersw  41972  hspval  42347