Theorem ifcli 4572

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

Syntax hints:   ∈ wcel 2107  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-if 4525

This theorem is referenced by:  ifex  4575  xaddf  13267  sadcf  16491  ramcl  17068  setcepi  18134  abvtrivd  20834  mvrf1  22007  mplcoe3  22057  psrbagsn  22088  evlslem1  22107  psdmplcl  22167  psdmul  22171  psdmvr  22174  marep01ma  22667  dscmet  24586  dscopn  24587  i1f1lem  25725  i1f1  25726  itg2const  25776  cxpval  26707  cxpcl  26717  recxpcl  26718  sqff1o  27226  chtublem  27256  dchrmullid  27297  bposlem1  27329  lgsval  27346  lgsfcl2  27348  lgscllem  27349  lgsval2lem  27352  lgsneg  27366  lgsdilem  27369  lgsdir2  27375  lgsdir  27377  lgsdi  27379  lgsne0  27380  dchrisum0flblem1  27553  dchrisum0flblem2  27554  dchrisum0fno1  27556  rpvmasum2  27557  omlsi  31424  indfval  32842  psgnfzto1stlem  33121  sgnsf  33183  ddemeas  34238  eulerpartlemb  34371  eulerpartlemgs2  34383  ex-sategoelel12  35433  sqdivzi  35729  poimirlem16  37644  poimirlem19  37647  pw2f1ocnv  43054  flcidc  43187  arearect  43232  sqrtcval  43659  sqrtcval2  43660  resqrtval  43661  imsqrtval  43662  limsup10exlem  45792  sqwvfourb  46249  fouriersw  46251  hspval  46629