Theorem ifcli 4524

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

Syntax hints:   ∈ wcel 2109  ifcif 4476

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 4477

This theorem is referenced by:  ifex  4527  xaddf  13126  sadcf  16364  ramcl  16941  setcepi  17995  abvtrivd  20717  mvrf1  21893  mplcoe3  21943  psrbagsn  21968  evlslem1  21987  psdmplcl  22047  psdmul  22051  psdmvr  22054  marep01ma  22545  dscmet  24458  dscopn  24459  i1f1lem  25588  i1f1  25589  itg2const  25639  cxpval  26571  cxpcl  26581  recxpcl  26582  sqff1o  27090  chtublem  27120  dchrmullid  27161  bposlem1  27193  lgsval  27210  lgsfcl2  27212  lgscllem  27213  lgsval2lem  27216  lgsneg  27230  lgsdilem  27233  lgsdir2  27239  lgsdir  27241  lgsdi  27243  lgsne0  27244  dchrisum0flblem1  27417  dchrisum0flblem2  27418  dchrisum0fno1  27420  rpvmasum2  27421  omlsi  31348  indfval  32800  psgnfzto1stlem  33043  sgnsf  33105  ddemeas  34209  eulerpartlemb  34342  eulerpartlemgs2  34354  ex-sategoelel12  35410  sqdivzi  35711  poimirlem16  37626  poimirlem19  37629  pw2f1ocnv  43020  flcidc  43153  arearect  43198  sqrtcval  43624  sqrtcval2  43625  resqrtval  43626  imsqrtval  43627  limsup10exlem  45763  sqwvfourb  46220  fouriersw  46222  hspval  46600