Theorem ifcli 4540

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

Syntax hints:   ∈ wcel 2149  ifcif 4492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4493

This theorem is referenced by:  ifex  4543  indfval  12225  xaddf  13250  sadcf  16511  ramcl  17089  setcepi  18145  abvtrivd  20913  mvrf1  22104  mplcoe3  22158  psrbagsn  22183  evlslem1  22202  psdmplcl  22294  psdmul  22298  psdmvr  22301  marep01ma  22786  dscmet  24698  dscopn  24699  i1f1lem  25817  i1f1  25818  itg2const  25868  cxpval  26795  cxpcl  26805  recxpcl  26806  sqff1o  27312  chtublem  27341  dchrmullid  27382  bposlem1  27414  lgsval  27431  lgsfcl2  27433  lgscllem  27434  lgsval2lem  27437  lgsneg  27451  lgsdilem  27454  lgsdir2  27460  lgsdir  27462  lgsdi  27464  lgsne0  27465  dchrisum0flblem1  27638  dchrisum0flblem2  27639  dchrisum0fno1  27641  rpvmasum2  27642  omlsi  31697  psgnfzto1stlem  33361  sgnsf  33423  ddemeas  34571  eulerpartlemb  34703  eulerpartlemgs2  34715  ex-sategoelel12  35852  sqdivzi  36153  poimirlem16  38209  poimirlem19  38212  pw2f1ocnv  43690  flcidc  43823  arearect  43868  sqrtcval  44293  sqrtcval2  44294  resqrtval  44295  imsqrtval  44296  limsup10exlem  46412  sqwvfourb  46869  fouriersw  46871  hspval  47249