Theorem ifcli 4515

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

Syntax hints:   ∈ wcel 2114  ifcif 4467

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  ifex  4518  indfval  12160  xaddf  13170  sadcf  16416  ramcl  16994  setcepi  18049  abvtrivd  20803  mvrf1  21977  mplcoe3  22029  psrbagsn  22054  evlslem1  22073  psdmplcl  22141  psdmul  22145  psdmvr  22148  marep01ma  22638  dscmet  24550  dscopn  24551  i1f1lem  25669  i1f1  25670  itg2const  25720  cxpval  26644  cxpcl  26654  recxpcl  26655  sqff1o  27162  chtublem  27191  dchrmullid  27232  bposlem1  27264  lgsval  27281  lgsfcl2  27283  lgscllem  27284  lgsval2lem  27287  lgsneg  27301  lgsdilem  27304  lgsdir2  27310  lgsdir  27312  lgsdi  27314  lgsne0  27315  dchrisum0flblem1  27488  dchrisum0flblem2  27489  dchrisum0fno1  27491  rpvmasum2  27492  omlsi  31493  psgnfzto1stlem  33179  sgnsf  33241  ddemeas  34399  eulerpartlemb  34531  eulerpartlemgs2  34543  ex-sategoelel12  35628  sqdivzi  35929  poimirlem16  37974  poimirlem19  37977  pw2f1ocnv  43486  flcidc  43619  arearect  43664  sqrtcval  44089  sqrtcval2  44090  resqrtval  44091  imsqrtval  44092  limsup10exlem  46221  sqwvfourb  46678  fouriersw  46680  hspval  47058