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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  ifex  4533  indfval  12327  xaddf  13354  sadcf  16623  ramcl  17207  setcepi  18263  abvtrivd  21089  mvrf1  22293  mplcoe3  22347  psrbagsn  22372  evlslem1  22391  psdmplcl  22483  psdmul  22487  psdmvr  22490  marep01ma  22975  dscmet  24891  dscopn  24892  i1f1lem  26010  i1f1  26011  itg2const  26061  cxpval  26992  cxpcl  27002  recxpcl  27003  sqff1o  27509  chtublem  27538  dchrmullid  27579  bposlem1  27611  lgsval  27628  lgsfcl2  27630  lgscllem  27631  lgsval2lem  27634  lgsneg  27648  lgsdilem  27651  lgsdir2  27657  lgsdir  27659  lgsdi  27661  lgsne0  27662  dchrisum0flblem1  27835  dchrisum0flblem2  27836  dchrisum0fno1  27838  rpvmasum2  27839  omlsi  32006  psgnfzto1stlem  33661  sgnsf  33723  ddemeas  34869  eulerpartlemb  35000  eulerpartlemgs2  35012  ex-sategoelel12  36192  sqdivzi  36493  poimirlem16  38554  poimirlem19  38557  pw2f1ocnv  44043  flcidc  44171  arearect  44216  sqrtcval  44640  sqrtcval2  44641  resqrtval  44642  imsqrtval  44643  limsup10exlem  46781  sqwvfourb  47238  fouriersw  47240  hspval  47618