Theorem ifcli 4531

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

Syntax hints:   ∈ wcel 2145  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  ifex  4534  indfval  12216  xaddf  13241  sadcf  16501  ramcl  17079  setcepi  18135  abvtrivd  20904  mvrf1  22095  mplcoe3  22149  psrbagsn  22174  evlslem1  22193  psdmplcl  22285  psdmul  22289  psdmvr  22292  marep01ma  22778  dscmet  24690  dscopn  24691  i1f1lem  25809  i1f1  25810  itg2const  25860  cxpval  26787  cxpcl  26797  recxpcl  26798  sqff1o  27304  chtublem  27333  dchrmullid  27374  bposlem1  27406  lgsval  27423  lgsfcl2  27425  lgscllem  27426  lgsval2lem  27429  lgsneg  27443  lgsdilem  27446  lgsdir2  27452  lgsdir  27454  lgsdi  27456  lgsne0  27457  dchrisum0flblem1  27630  dchrisum0flblem2  27631  dchrisum0fno1  27633  rpvmasum2  27634  omlsi  31665  psgnfzto1stlem  33333  sgnsf  33395  ddemeas  34543  eulerpartlemb  34675  eulerpartlemgs2  34687  ex-sategoelel12  35790  sqdivzi  36091  poimirlem16  38147  poimirlem19  38150  pw2f1ocnv  43626  flcidc  43759  arearect  43804  sqrtcval  44229  sqrtcval2  44230  resqrtval  44231  imsqrtval  44232  limsup10exlem  46344  sqwvfourb  46801  fouriersw  46803  hspval  47181