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

Theorem ifcli 4485
Description: Inference associated with ifcl 4483. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4495 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 4483 . 2 ((𝐴𝐶𝐵𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
41, 2, 3mp2an 691 1 if(𝜑, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2114  ifcif 4439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-if 4440
This theorem is referenced by:  ifex  4487  xaddf  12605  sadcf  15791  ramcl  16354  setcepi  17339  abvtrivd  19602  mvrf1  20661  mplcoe3  20704  psrbagsn  20732  evlslem1  20752  marep01ma  21263  dscmet  23177  dscopn  23178  i1f1lem  24291  i1f1  24292  itg2const  24342  cxpval  25253  cxpcl  25263  recxpcl  25264  sqff1o  25765  chtublem  25793  dchrmulid2  25834  bposlem1  25866  lgsval  25883  lgsfcl2  25885  lgscllem  25886  lgsval2lem  25889  lgsneg  25903  lgsdilem  25906  lgsdir2  25912  lgsdir  25914  lgsdi  25916  lgsne0  25917  dchrisum0flblem1  26090  dchrisum0flblem2  26091  dchrisum0fno1  26093  rpvmasum2  26094  omlsi  29185  psgnfzto1stlem  30773  sgnsf  30835  indfval  31349  ddemeas  31569  eulerpartlemb  31700  eulerpartlemgs2  31712  ex-sategoelel12  32748  sqdivzi  33033  poimirlem16  35032  poimirlem19  35035  pw2f1ocnv  39909  flcidc  40049  arearect  40096  sqrtcval  40272  sqrtcval2  40273  resqrtval  40274  imsqrtval  40275  limsup10exlem  42354  sqwvfourb  42811  fouriersw  42813  hspval  43188
  Copyright terms: Public domain W3C validator