Theorem ifcli 4535

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

Syntax hints:   ∈ wcel 2143  ifcif 4487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4488

This theorem is referenced by:  ifex  4538  indfval  12220  xaddf  13245  sadcf  16506  ramcl  17084  setcepi  18140  abvtrivd  20935  mvrf1  22135  mplcoe3  22189  psrbagsn  22214  evlslem1  22233  psdmplcl  22325  psdmul  22329  psdmvr  22332  marep01ma  22817  dscmet  24729  dscopn  24730  i1f1lem  25848  i1f1  25849  itg2const  25899  cxpval  26829  cxpcl  26839  recxpcl  26840  sqff1o  27346  chtublem  27375  dchrmullid  27416  bposlem1  27448  lgsval  27465  lgsfcl2  27467  lgscllem  27468  lgsval2lem  27471  lgsneg  27485  lgsdilem  27488  lgsdir2  27494  lgsdir  27496  lgsdi  27498  lgsne0  27499  dchrisum0flblem1  27672  dchrisum0flblem2  27673  dchrisum0fno1  27675  rpvmasum2  27676  omlsi  31756  psgnfzto1stlem  33420  sgnsf  33482  ddemeas  34626  eulerpartlemb  34758  eulerpartlemgs2  34770  ex-sategoelel12  35919  sqdivzi  36220  poimirlem16  38307  poimirlem19  38310  pw2f1ocnv  43784  flcidc  43917  arearect  43962  sqrtcval  44387  sqrtcval2  44388  resqrtval  44389  imsqrtval  44390  limsup10exlem  46506  sqwvfourb  46963  fouriersw  46965  hspval  47343  crosspclifi  50659