Theorem ifcli 4527

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

Syntax hints:   ∈ wcel 2113  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  ifex  4530  xaddf  13141  sadcf  16382  ramcl  16959  setcepi  18014  abvtrivd  20767  mvrf1  21943  mplcoe3  21995  psrbagsn  22020  evlslem1  22039  psdmplcl  22107  psdmul  22111  psdmvr  22114  marep01ma  22606  dscmet  24518  dscopn  24519  i1f1lem  25648  i1f1  25649  itg2const  25699  cxpval  26631  cxpcl  26641  recxpcl  26642  sqff1o  27150  chtublem  27180  dchrmullid  27221  bposlem1  27253  lgsval  27270  lgsfcl2  27272  lgscllem  27273  lgsval2lem  27276  lgsneg  27290  lgsdilem  27293  lgsdir2  27299  lgsdir  27301  lgsdi  27303  lgsne0  27304  dchrisum0flblem1  27477  dchrisum0flblem2  27478  dchrisum0fno1  27480  rpvmasum2  27481  omlsi  31481  indfval  32937  psgnfzto1stlem  33184  sgnsf  33246  ddemeas  34395  eulerpartlemb  34527  eulerpartlemgs2  34539  ex-sategoelel12  35623  sqdivzi  35924  poimirlem16  37839  poimirlem19  37842  pw2f1ocnv  43300  flcidc  43433  arearect  43478  sqrtcval  43903  sqrtcval2  43904  resqrtval  43905  imsqrtval  43906  limsup10exlem  46037  sqwvfourb  46494  fouriersw  46496  hspval  46874