Theorem ifcli 4529

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

Syntax hints:   ∈ wcel 2114  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  ifex  4532  xaddf  13151  sadcf  16392  ramcl  16969  setcepi  18024  abvtrivd  20780  mvrf1  21956  mplcoe3  22008  psrbagsn  22033  evlslem1  22052  psdmplcl  22120  psdmul  22124  psdmvr  22127  marep01ma  22619  dscmet  24531  dscopn  24532  i1f1lem  25661  i1f1  25662  itg2const  25712  cxpval  26644  cxpcl  26654  recxpcl  26655  sqff1o  27163  chtublem  27193  dchrmullid  27234  bposlem1  27266  lgsval  27283  lgsfcl2  27285  lgscllem  27286  lgsval2lem  27289  lgsneg  27303  lgsdilem  27306  lgsdir2  27312  lgsdir  27314  lgsdi  27316  lgsne0  27317  dchrisum0flblem1  27490  dchrisum0flblem2  27491  dchrisum0fno1  27493  rpvmasum2  27494  omlsi  31496  indfval  32950  psgnfzto1stlem  33198  sgnsf  33260  ddemeas  34418  eulerpartlemb  34550  eulerpartlemgs2  34562  ex-sategoelel12  35647  sqdivzi  35948  poimirlem16  37891  poimirlem19  37894  pw2f1ocnv  43398  flcidc  43531  arearect  43576  sqrtcval  44001  sqrtcval2  44002  resqrtval  44003  imsqrtval  44004  limsup10exlem  46134  sqwvfourb  46591  fouriersw  46593  hspval  46971