Theorem ifcli 4471

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

Syntax hints:   ∈ wcel 2111  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426

This theorem is referenced by:  ifex  4473  xaddf  12605  sadcf  15792  ramcl  16355  setcepi  17340  abvtrivd  19604  mvrf1  20663  mplcoe3  20706  psrbagsn  20734  evlslem1  20754  marep01ma  21265  dscmet  23179  dscopn  23180  i1f1lem  24293  i1f1  24294  itg2const  24344  cxpval  25255  cxpcl  25265  recxpcl  25266  sqff1o  25767  chtublem  25795  dchrmulid2  25836  bposlem1  25868  lgsval  25885  lgsfcl2  25887  lgscllem  25888  lgsval2lem  25891  lgsneg  25905  lgsdilem  25908  lgsdir2  25914  lgsdir  25916  lgsdi  25918  lgsne0  25919  dchrisum0flblem1  26092  dchrisum0flblem2  26093  dchrisum0fno1  26095  rpvmasum2  26096  omlsi  29187  psgnfzto1stlem  30792  sgnsf  30854  indfval  31385  ddemeas  31605  eulerpartlemb  31736  eulerpartlemgs2  31748  ex-sategoelel12  32787  sqdivzi  33072  poimirlem16  35073  poimirlem19  35076  pw2f1ocnv  39978  flcidc  40118  arearect  40165  sqrtcval  40341  sqrtcval2  40342  resqrtval  40343  imsqrtval  40344  limsup10exlem  42414  sqwvfourb  42871  fouriersw  42873  hspval  43248