Theorem ifcli 4503

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

Syntax hints:   ∈ wcel 2108  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  ifex  4506  xaddf  12887  sadcf  16088  ramcl  16658  setcepi  17719  abvtrivd  20015  mvrf1  21104  mplcoe3  21149  psrbagsn  21181  evlslem1  21202  marep01ma  21717  dscmet  23634  dscopn  23635  i1f1lem  24758  i1f1  24759  itg2const  24810  cxpval  25724  cxpcl  25734  recxpcl  25735  sqff1o  26236  chtublem  26264  dchrmulid2  26305  bposlem1  26337  lgsval  26354  lgsfcl2  26356  lgscllem  26357  lgsval2lem  26360  lgsneg  26374  lgsdilem  26377  lgsdir2  26383  lgsdir  26385  lgsdi  26387  lgsne0  26388  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0fno1  26564  rpvmasum2  26565  omlsi  29667  psgnfzto1stlem  31269  sgnsf  31331  indfval  31884  ddemeas  32104  eulerpartlemb  32235  eulerpartlemgs2  32247  ex-sategoelel12  33289  sqdivzi  33599  poimirlem16  35720  poimirlem19  35723  pw2f1ocnv  40775  flcidc  40915  arearect  40962  sqrtcval  41138  sqrtcval2  41139  resqrtval  41140  imsqrtval  41141  limsup10exlem  43203  sqwvfourb  43660  fouriersw  43662  hspval  44037