Theorem ifcli 4537

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4490

This theorem is used by:  ifex  4540  indfval  12242  xaddf  13268  sadcf  16535  ramcl  17113  setcepi  18169  abvtrivd  20987  mvrf1  22187  mplcoe3  22241  psrbagsn  22266  evlslem1  22285  psdmplcl  22377  psdmul  22381  psdmvr  22384  marep01ma  22869  dscmet  24782  dscopn  24783  i1f1lem  25901  i1f1  25902  itg2const  25952  cxpval  26882  cxpcl  26892  recxpcl  26893  sqff1o  27399  chtublem  27428  dchrmullid  27469  bposlem1  27501  lgsval  27518  lgsfcl2  27520  lgscllem  27521  lgsval2lem  27524  lgsneg  27538  lgsdilem  27541  lgsdir2  27547  lgsdir  27549  lgsdi  27551  lgsne0  27552  dchrisum0flblem1  27725  dchrisum0flblem2  27726  dchrisum0fno1  27728  rpvmasum2  27729  omlsi  31829  psgnfzto1stlem  33486  sgnsf  33548  ddemeas  34693  eulerpartlemb  34825  eulerpartlemgs2  34837  ex-sategoelel12  35958  sqdivzi  36259  poimirlem16  38346  poimirlem19  38349  pw2f1ocnv  43824  flcidc  43957  arearect  44002  sqrtcval  44427  sqrtcval2  44428  resqrtval  44429  imsqrtval  44430  limsup10exlem  46546  sqwvfourb  47003  fouriersw  47005  hspval  47383