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

Theorem ifcli 4537
Description: Inference associated with ifcl 4535. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4548 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 4535 . 2 ((𝐴𝐶𝐵𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
41, 2, 3mp2an 691 1 if(𝜑, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  ifcif 4490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4491
This theorem is referenced by:  ifex  4540  xaddf  13152  sadcf  16341  ramcl  16909  setcepi  17982  abvtrivd  20342  mvrf1  21417  mplcoe3  21462  psrbagsn  21494  evlslem1  21515  marep01ma  22032  dscmet  23951  dscopn  23952  i1f1lem  25076  i1f1  25077  itg2const  25128  cxpval  26042  cxpcl  26052  recxpcl  26053  sqff1o  26554  chtublem  26582  dchrmullid  26623  bposlem1  26655  lgsval  26672  lgsfcl2  26674  lgscllem  26675  lgsval2lem  26678  lgsneg  26692  lgsdilem  26695  lgsdir2  26701  lgsdir  26703  lgsdi  26705  lgsne0  26706  dchrisum0flblem1  26879  dchrisum0flblem2  26880  dchrisum0fno1  26882  rpvmasum2  26883  omlsi  30395  psgnfzto1stlem  32005  sgnsf  32067  indfval  32679  ddemeas  32899  eulerpartlemb  33032  eulerpartlemgs2  33044  ex-sategoelel12  34085  sqdivzi  34363  poimirlem16  36144  poimirlem19  36147  pw2f1ocnv  41408  flcidc  41548  arearect  41596  sqrtcval  42005  sqrtcval2  42006  resqrtval  42007  imsqrtval  42008  limsup10exlem  44103  sqwvfourb  44560  fouriersw  44562  hspval  44940
  Copyright terms: Public domain W3C validator