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

Theorem ifclda 4522
Description: Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
ifclda.1 ((𝜑𝜓) → 𝐴𝐶)
ifclda.2 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
Assertion
Ref Expression
ifclda (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifclda
StepHypRef Expression
1 iftrue 4493 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 483 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifclda.1 . . 3 ((𝜑𝜓) → 𝐴𝐶)
42, 3eqeltrd 2838 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5 iffalse 4496 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 483 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifclda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
86, 7eqeltrd 2838 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
94, 8pm2.61dan 812 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  wcel 2107  ifcif 4487
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-if 4488
This theorem is referenced by:  unxpdomlem3  9197  updjudhf  9868  acndom  9988  iunfictbso  10051  dfac12lem2  10081  ttukeylem6  10451  canthp1lem2  10590  xaddf  13144  xmulf  13192  ccatcl  14463  swrdcl  14534  ccatco  14725  lo1bdd2  15407  o1lo1  15420  sadadd2lem2  16331  sadcaddlem  16338  sadadd2lem  16340  sadadd3  16342  lcmfval  16498  iserodd  16708  prmreclem2  16790  prmreclem4  16792  prmreclem6  16794  prmrec  16795  vdwlem6  16859  mreexexd  17529  smndex2hbas  18727  symgextf  19200  pmtrf  19238  odfval  19315  cyggex2  19675  dprdfid  19797  dmdprdsplitlem  19817  sdrgacs  20271  cygznlem1  20976  cygznlem2a  20977  cygznlem3  20979  cygth  20981  fvmptnn04if  22201  chfacfisf  22206  chfacfisfcpmat  22207  ptpjpre2  22934  ptopn2  22938  ptpjopn  22966  iccpnfcnv  24310  xrhmeo  24312  cmetcaulem  24655  ovolunlem1a  24863  ovolunlem1  24864  ioorf  24940  mbfi1fseqlem3  25085  mbfi1flim  25091  itg2seq  25110  itg2splitlem  25116  itg2split  25117  iblss  25172  itgle  25177  itgeqa  25181  ibladdlem  25187  itgaddlem1  25190  iblabslem  25195  iblabs  25196  iblabsr  25197  iblmulc2  25198  itgmulc2lem1  25199  bddmulibl  25206  bddiblnc  25209  itggt0  25211  itgcn  25212  ellimc2  25244  limccnp  25258  limccnp2  25259  dvcobr  25313  lhop1  25381  elplyd  25566  coeeq2  25606  dvply1  25647  aalioulem3  25697  dvtaylp  25732  dvradcnv  25783  psercnlem1  25787  logcnlem2  26001  logcnlem3  26002  logcnlem4  26003  logtayllem  26017  logtayl  26018  cxpcl  26032  recxpcl  26033  leibpilem2  26294  leibpi  26295  rlimcnp2  26319  efrlim  26322  igamf  26403  igamcl  26404  pclogsum  26566  dchrelbasd  26590  lgsfcl2  26654  lgscllem  26655  lgsval2lem  26658  lgsne0  26686  2sqnn0  26789  dchrvmasumiflem2  26853  dchrisum0flblem1  26859  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntlemj  26954  padicabv  26981  crctcshwlkn0  28769  sgnsval  32013  xrge0iifcnv  32517  xrge0iifhom  32521  pnfneige0  32535  esumpinfval  32675  sigaclfu2  32723  ballotlemsv  33112  ballotlemsdom  33114  signswmnd  33172  signsvvf  33194  signsvfn  33197  mrsubcv  34107  mrsubff  34109  mrsubrn  34110  mrsubccat  34115  unblimceq0lem  34972  ptrecube  36081  poimirlem24  36105  itg2addnclem2  36133  itg2gt0cn  36136  ibladdnclem  36137  itgaddnclem1  36139  iblabsnclem  36144  iblabsnc  36145  iblmulc2nc  36146  itgmulc2nclem1  36147  itggt0cn  36151  ftc1anclem5  36158  ftc1anclem6  36159  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  areacirc  36174  cdleme27cl  38832  selvcllem5  40763  dffltz  40975  cantnfub  41658  climsuse  43856  lptioo1  43880  icccncfext  44135  cncfiooicclem1  44141  iblsplit  44214  dirkerval2  44342  dirkerre  44343  fourierdlem9  44364  fourierdlem17  44372  fourierdlem43  44398  etransclem3  44485  etransclem7  44489  etransclem10  44492  etransclem21  44503  lincext1  46542
  Copyright terms: Public domain W3C validator