Theorem ifcli 4530

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

This proof depends on syntax axioms:   ∈ wcel 2145  ifcif 4482

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4483

This theorem is used by:  ifex  4533  indfval  12252  xaddf  13279  sadcf  16546  ramcl  17124  setcepi  18180  abvtrivd  21001  mvrf1  22203  mplcoe3  22257  psrbagsn  22282  evlslem1  22301  psdmplcl  22393  psdmul  22397  psdmvr  22400  marep01ma  22885  dscmet  24801  dscopn  24802  i1f1lem  25920  i1f1  25921  itg2const  25971  cxpval  26904  cxpcl  26914  recxpcl  26915  sqff1o  27421  chtublem  27450  dchrmullid  27491  bposlem1  27523  lgsval  27540  lgsfcl2  27542  lgscllem  27543  lgsval2lem  27546  lgsneg  27560  lgsdilem  27563  lgsdir2  27569  lgsdir  27571  lgsdi  27573  lgsne0  27574  dchrisum0flblem1  27747  dchrisum0flblem2  27748  dchrisum0fno1  27750  rpvmasum2  27751  omlsi  31888  psgnfzto1stlem  33543  sgnsf  33605  ddemeas  34750  eulerpartlemb  34882  eulerpartlemgs2  34894  ex-sategoelel12  36009  sqdivzi  36310  poimirlem16  38388  poimirlem19  38391  pw2f1ocnv  43881  flcidc  44014  arearect  44059  sqrtcval  44484  sqrtcval2  44485  resqrtval  44486  imsqrtval  44487  limsup10exlem  46603  sqwvfourb  47060  fouriersw  47062  hspval  47440