Theorem ifcli 4595

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

Syntax hints:   ∈ wcel 2108  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  ifex  4598  xaddf  13286  sadcf  16499  ramcl  17076  setcepi  18155  abvtrivd  20855  mvrf1  22029  mplcoe3  22079  psrbagsn  22110  evlslem1  22129  psdmplcl  22189  psdmul  22193  marep01ma  22687  dscmet  24606  dscopn  24607  i1f1lem  25743  i1f1  25744  itg2const  25795  cxpval  26724  cxpcl  26734  recxpcl  26735  sqff1o  27243  chtublem  27273  dchrmullid  27314  bposlem1  27346  lgsval  27363  lgsfcl2  27365  lgscllem  27366  lgsval2lem  27369  lgsneg  27383  lgsdilem  27386  lgsdir2  27392  lgsdir  27394  lgsdi  27396  lgsne0  27397  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0fno1  27573  rpvmasum2  27574  omlsi  31436  psgnfzto1stlem  33093  sgnsf  33155  indfval  33980  ddemeas  34200  eulerpartlemb  34333  eulerpartlemgs2  34345  ex-sategoelel12  35395  sqdivzi  35690  poimirlem16  37596  poimirlem19  37599  pw2f1ocnv  42994  flcidc  43131  arearect  43176  sqrtcval  43603  sqrtcval2  43604  resqrtval  43605  imsqrtval  43606  limsup10exlem  45693  sqwvfourb  46150  fouriersw  46152  hspval  46530