Theorem ifcli 4532

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

Syntax hints:   ∈ wcel 2109  ifcif 4484

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4485

This theorem is referenced by:  ifex  4535  xaddf  13160  sadcf  16399  ramcl  16976  setcepi  18030  abvtrivd  20752  mvrf1  21928  mplcoe3  21978  psrbagsn  22003  evlslem1  22022  psdmplcl  22082  psdmul  22086  psdmvr  22089  marep01ma  22580  dscmet  24493  dscopn  24494  i1f1lem  25623  i1f1  25624  itg2const  25674  cxpval  26606  cxpcl  26616  recxpcl  26617  sqff1o  27125  chtublem  27155  dchrmullid  27196  bposlem1  27228  lgsval  27245  lgsfcl2  27247  lgscllem  27248  lgsval2lem  27251  lgsneg  27265  lgsdilem  27268  lgsdir2  27274  lgsdir  27276  lgsdi  27278  lgsne0  27279  dchrisum0flblem1  27452  dchrisum0flblem2  27453  dchrisum0fno1  27455  rpvmasum2  27456  omlsi  31383  indfval  32829  psgnfzto1stlem  33072  sgnsf  33134  ddemeas  34219  eulerpartlemb  34352  eulerpartlemgs2  34364  ex-sategoelel12  35407  sqdivzi  35708  poimirlem16  37623  poimirlem19  37626  pw2f1ocnv  43019  flcidc  43152  arearect  43197  sqrtcval  43623  sqrtcval2  43624  resqrtval  43625  imsqrtval  43626  limsup10exlem  45763  sqwvfourb  46220  fouriersw  46222  hspval  46600