Theorem ifcli 4532

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

This proof depends on syntax axioms:   ∈ wcel 2146  ifcif 4484

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4485

This theorem is used by:  ifex  4535  indfval  12337  xaddf  13364  sadcf  16635  ramcl  17219  setcepi  18275  abvtrivd  21101  mvrf1  22305  mplcoe3  22359  psrbagsn  22384  evlslem1  22403  psdmplcl  22495  psdmul  22499  psdmvr  22502  marep01ma  22987  dscmet  24903  dscopn  24904  i1f1lem  26022  i1f1  26023  itg2const  26073  cxpval  27004  cxpcl  27014  recxpcl  27015  sqff1o  27521  chtublem  27550  dchrmullid  27591  bposlem1  27623  lgsval  27640  lgsfcl2  27642  lgscllem  27643  lgsval2lem  27646  lgsneg  27660  lgsdilem  27663  lgsdir2  27669  lgsdir  27671  lgsdi  27673  lgsne0  27674  dchrisum0flblem1  27847  dchrisum0flblem2  27848  dchrisum0fno1  27850  rpvmasum2  27851  omlsi  32018  psgnfzto1stlem  33714  sgnsf  33776  ddemeas  34922  eulerpartlemb  35053  eulerpartlemgs2  35065  ex-sategoelel12  36313  sqdivzi  36620  poimirlem16  38694  poimirlem19  38697  pw2f1ocnv  44184  flcidc  44312  arearect  44357  sqrtcval  44781  sqrtcval2  44782  resqrtval  44783  imsqrtval  44784  limsup10exlem  46921  sqwvfourb  47378  fouriersw  47380  hspval  47758  parswapprop  50916