Theorem ifcli 4538

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

Syntax hints:   ∈ wcel 2109  ifcif 4490

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4491

This theorem is referenced by:  ifex  4541  xaddf  13190  sadcf  16429  ramcl  17006  setcepi  18056  abvtrivd  20747  mvrf1  21901  mplcoe3  21951  psrbagsn  21976  evlslem1  21995  psdmplcl  22055  psdmul  22059  psdmvr  22062  marep01ma  22553  dscmet  24466  dscopn  24467  i1f1lem  25596  i1f1  25597  itg2const  25647  cxpval  26579  cxpcl  26589  recxpcl  26590  sqff1o  27098  chtublem  27128  dchrmullid  27169  bposlem1  27201  lgsval  27218  lgsfcl2  27220  lgscllem  27221  lgsval2lem  27224  lgsneg  27238  lgsdilem  27241  lgsdir2  27247  lgsdir  27249  lgsdi  27251  lgsne0  27252  dchrisum0flblem1  27425  dchrisum0flblem2  27426  dchrisum0fno1  27428  rpvmasum2  27429  omlsi  31339  indfval  32785  psgnfzto1stlem  33063  sgnsf  33125  ddemeas  34232  eulerpartlemb  34365  eulerpartlemgs2  34377  ex-sategoelel12  35414  sqdivzi  35710  poimirlem16  37625  poimirlem19  37628  pw2f1ocnv  43019  flcidc  43152  arearect  43197  sqrtcval  43623  sqrtcval2  43624  resqrtval  43625  imsqrtval  43626  limsup10exlem  45763  sqwvfourb  46220  fouriersw  46222  hspval  46600