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

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
StepHypRef Expression
1 ifcli.1 . 2 𝐴𝐶
2 ifcli.2 . 2 𝐵𝐶
3 ifcl 4529 . 2 ((𝐴𝐶𝐵𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
41, 2, 3mp2an 690 1 if(𝜑, 𝐴, 𝐵) ∈ 𝐶
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  ifcif 4484
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-if 4485
This theorem is referenced by:  ifex  4534  xaddf  13135  sadcf  16325  ramcl  16893  setcepi  17966  abvtrivd  20284  mvrf1  21378  mplcoe3  21423  psrbagsn  21455  evlslem1  21476  marep01ma  21993  dscmet  23912  dscopn  23913  i1f1lem  25037  i1f1  25038  itg2const  25089  cxpval  26003  cxpcl  26013  recxpcl  26014  sqff1o  26515  chtublem  26543  dchrmulid2  26584  bposlem1  26616  lgsval  26633  lgsfcl2  26635  lgscllem  26636  lgsval2lem  26639  lgsneg  26653  lgsdilem  26656  lgsdir2  26662  lgsdir  26664  lgsdi  26666  lgsne0  26667  dchrisum0flblem1  26840  dchrisum0flblem2  26841  dchrisum0fno1  26843  rpvmasum2  26844  omlsi  30232  psgnfzto1stlem  31832  sgnsf  31894  indfval  32484  ddemeas  32704  eulerpartlemb  32837  eulerpartlemgs2  32849  ex-sategoelel12  33890  sqdivzi  34170  poimirlem16  36061  poimirlem19  36064  pw2f1ocnv  41299  flcidc  41439  arearect  41487  sqrtcval  41855  sqrtcval2  41856  resqrtval  41857  imsqrtval  41858  limsup10exlem  43945  sqwvfourb  44402  fouriersw  44404  hspval  44782
  Copyright terms: Public domain W3C validator