Theorem ifcli 4576

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

Syntax hints:   ∈ wcel 2107  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  ifex  4579  xaddf  13203  sadcf  16394  ramcl  16962  setcepi  18038  abvtrivd  20448  mvrf1  21545  mplcoe3  21593  psrbagsn  21624  evlslem1  21645  marep01ma  22162  dscmet  24081  dscopn  24082  i1f1lem  25206  i1f1  25207  itg2const  25258  cxpval  26172  cxpcl  26182  recxpcl  26183  sqff1o  26686  chtublem  26714  dchrmullid  26755  bposlem1  26787  lgsval  26804  lgsfcl2  26806  lgscllem  26807  lgsval2lem  26810  lgsneg  26824  lgsdilem  26827  lgsdir2  26833  lgsdir  26835  lgsdi  26837  lgsne0  26838  dchrisum0flblem1  27011  dchrisum0flblem2  27012  dchrisum0fno1  27014  rpvmasum2  27015  omlsi  30657  psgnfzto1stlem  32259  sgnsf  32321  indfval  33014  ddemeas  33234  eulerpartlemb  33367  eulerpartlemgs2  33379  ex-sategoelel12  34418  sqdivzi  34697  poimirlem16  36504  poimirlem19  36507  pw2f1ocnv  41776  flcidc  41916  arearect  41964  sqrtcval  42392  sqrtcval2  42393  resqrtval  42394  imsqrtval  42395  limsup10exlem  44488  sqwvfourb  44945  fouriersw  44947  hspval  45325