Theorem ifcli 4528

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

Syntax hints:   ∈ wcel 2142  ifcif 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4481

This theorem is referenced by:  ifex  4531  indfval  12202  xaddf  13227  sadcf  16487  ramcl  17065  setcepi  18121  abvtrivd  20881  mvrf1  22037  mplcoe3  22091  psrbagsn  22116  evlslem1  22135  psdmplcl  22227  psdmul  22231  psdmvr  22234  marep01ma  22720  dscmet  24632  dscopn  24633  i1f1lem  25751  i1f1  25752  itg2const  25802  cxpval  26729  cxpcl  26739  recxpcl  26740  sqff1o  27246  chtublem  27275  dchrmullid  27316  bposlem1  27348  lgsval  27365  lgsfcl2  27367  lgscllem  27368  lgsval2lem  27371  lgsneg  27385  lgsdilem  27388  lgsdir2  27394  lgsdir  27396  lgsdi  27398  lgsne0  27399  dchrisum0flblem1  27572  dchrisum0flblem2  27573  dchrisum0fno1  27575  rpvmasum2  27576  omlsi  31607  psgnfzto1stlem  33280  sgnsf  33342  ddemeas  34533  eulerpartlemb  34665  eulerpartlemgs2  34677  ex-sategoelel12  35777  sqdivzi  36078  poimirlem16  38135  poimirlem19  38138  pw2f1ocnv  43614  flcidc  43747  arearect  43792  sqrtcval  44217  sqrtcval2  44218  resqrtval  44219  imsqrtval  44220  limsup10exlem  46346  sqwvfourb  46803  fouriersw  46805  hspval  47183