MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifcli Structured version   Visualization version   GIF version

Theorem ifcli 4390
Description: Inference associated with ifcl 4388. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4400 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
StepHypRef Expression
1 ifcli.1 . 2 𝐴𝐶
2 ifcli.2 . 2 𝐵𝐶
3 ifcl 4388 . 2 ((𝐴𝐶𝐵𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
41, 2, 3mp2an 679 1 if(𝜑, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2050  ifcif 4344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2744
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-if 4345
This theorem is referenced by:  ifex  4392  xaddf  12432  sadcf  15660  ramcl  16219  setcepi  17218  abvtrivd  19345  mvrf1  19931  mplcoe3  19972  psrbagsn  20000  evlslem1  20020  marep01ma  20985  dscmet  22897  dscopn  22898  i1f1lem  24005  i1f1  24006  itg2const  24056  cxpval  24960  cxpcl  24970  recxpcl  24971  sqff1o  25473  chtublem  25501  dchrmulid2  25542  bposlem1  25574  lgsval  25591  lgsfcl2  25593  lgscllem  25594  lgsval2lem  25597  lgsneg  25611  lgsdilem  25614  lgsdir2  25620  lgsdir  25622  lgsdi  25624  lgsne0  25625  dchrisum0flblem1  25798  dchrisum0flblem2  25799  dchrisum0fno1  25801  rpvmasum2  25802  omlsi  28974  sgnsf  30499  psgnfzto1stlem  30720  indfval  30948  ddemeas  31169  eulerpartlemb  31300  eulerpartlemgs2  31312  sqdivzi  32508  poimirlem16  34378  poimirlem19  34381  pw2f1ocnv  39059  flcidc  39199  arearect  39247  limsup10exlem  41509  sqwvfourb  41970  fouriersw  41972  hspval  42347
  Copyright terms: Public domain W3C validator