Theorem ifcli 4553

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

Syntax hints:   ∈ wcel 2109  ifcif 4505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-if 4506

This theorem is referenced by:  ifex  4556  xaddf  13245  sadcf  16477  ramcl  17054  setcepi  18106  abvtrivd  20797  mvrf1  21951  mplcoe3  22001  psrbagsn  22026  evlslem1  22045  psdmplcl  22105  psdmul  22109  psdmvr  22112  marep01ma  22603  dscmet  24516  dscopn  24517  i1f1lem  25647  i1f1  25648  itg2const  25698  cxpval  26630  cxpcl  26640  recxpcl  26641  sqff1o  27149  chtublem  27179  dchrmullid  27220  bposlem1  27252  lgsval  27269  lgsfcl2  27271  lgscllem  27272  lgsval2lem  27275  lgsneg  27289  lgsdilem  27292  lgsdir2  27298  lgsdir  27300  lgsdi  27302  lgsne0  27303  dchrisum0flblem1  27476  dchrisum0flblem2  27477  dchrisum0fno1  27479  rpvmasum2  27480  omlsi  31390  indfval  32838  psgnfzto1stlem  33116  sgnsf  33178  ddemeas  34272  eulerpartlemb  34405  eulerpartlemgs2  34417  ex-sategoelel12  35454  sqdivzi  35750  poimirlem16  37665  poimirlem19  37668  pw2f1ocnv  43028  flcidc  43161  arearect  43206  sqrtcval  43632  sqrtcval2  43633  resqrtval  43634  imsqrtval  43635  limsup10exlem  45768  sqwvfourb  46225  fouriersw  46227  hspval  46605