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

Theorem ifclda 4484
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 4456 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 485 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifclda.1 . . 3 ((𝜑𝜓) → 𝐴𝐶)
42, 3eqeltrd 2916 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5 iffalse 4459 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 485 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifclda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
86, 7eqeltrd 2916 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
94, 8pm2.61dan 812 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1538  wcel 2115  ifcif 4450
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-if 4451
This theorem is referenced by:  unxpdomlem3  8721  updjudhf  9357  acndom  9475  iunfictbso  9538  dfac12lem2  9568  ttukeylem6  9934  canthp1lem2  10073  xaddf  12614  xmulf  12662  ccatcl  13926  swrdcl  14007  ccatco  14197  lo1bdd2  14881  o1lo1  14894  sadadd2lem2  15797  sadcaddlem  15804  sadadd2lem  15806  sadadd3  15808  lcmfval  15963  iserodd  16170  prmreclem2  16251  prmreclem4  16253  prmreclem6  16255  prmrec  16256  vdwlem6  16320  mreexexd  16919  smndex2hbas  18081  symgextf  18545  pmtrf  18583  odfval  18660  cyggex2  19017  dprdfid  19139  dmdprdsplitlem  19159  sdrgacs  19580  cygznlem1  20713  cygznlem2a  20714  cygznlem3  20716  cygth  20718  fvmptnn04if  21457  chfacfisf  21462  chfacfisfcpmat  21463  ptpjpre2  22188  ptopn2  22192  ptpjopn  22220  iccpnfcnv  23552  xrhmeo  23554  cmetcaulem  23895  ovolunlem1a  24103  ovolunlem1  24104  ioorf  24180  mbfi1fseqlem3  24324  mbfi1flim  24330  itg2seq  24349  itg2splitlem  24355  itg2split  24356  iblss  24411  itgle  24416  itgeqa  24420  ibladdlem  24426  itgaddlem1  24429  iblabslem  24434  iblabs  24435  iblabsr  24436  iblmulc2  24437  itgmulc2lem1  24438  bddmulibl  24445  bddiblnc  24448  itggt0  24450  itgcn  24451  ellimc2  24483  limccnp  24497  limccnp2  24498  dvcobr  24552  lhop1  24620  elplyd  24802  coeeq2  24842  dvply1  24883  aalioulem3  24933  dvtaylp  24968  dvradcnv  25019  psercnlem1  25023  logcnlem2  25237  logcnlem3  25238  logcnlem4  25239  logtayllem  25253  logtayl  25254  cxpcl  25268  recxpcl  25269  leibpilem2  25530  leibpi  25531  rlimcnp2  25555  efrlim  25558  igamf  25639  igamcl  25640  pclogsum  25802  dchrelbasd  25826  lgsfcl2  25890  lgscllem  25891  lgsval2lem  25894  lgsne0  25922  2sqnn0  26025  dchrvmasumiflem2  26089  dchrisum0flblem1  26095  pntrlog2bndlem4  26167  pntrlog2bndlem5  26168  pntlemj  26190  padicabv  26217  crctcshwlkn0  27610  sgnsval  30835  xrge0iifcnv  31233  xrge0iifhom  31237  pnfneige0  31251  esumpinfval  31389  sigaclfu2  31437  ballotlemsv  31824  ballotlemsdom  31826  signswmnd  31884  signsvvf  31906  signsvfn  31909  mrsubcv  32814  mrsubff  32816  mrsubrn  32817  mrsubccat  32822  unblimceq0lem  33902  ptrecube  35002  poimirlem24  35026  itg2addnclem2  35054  itg2gt0cn  35057  ibladdnclem  35058  itgaddnclem1  35060  iblabsnclem  35065  iblabsnc  35066  iblmulc2nc  35067  itgmulc2nclem1  35068  itggt0cn  35072  ftc1anclem5  35079  ftc1anclem6  35080  ftc1anclem7  35081  ftc1anclem8  35082  ftc1anc  35083  areacirc  35095  cdleme27cl  37607  selvval2lem5  39365  dffltz  39531  climsuse  42176  lptioo1  42200  icccncfext  42455  cncfiooicclem1  42461  iblsplit  42534  dirkerval2  42662  dirkerre  42663  fourierdlem9  42684  fourierdlem17  42692  fourierdlem43  42718  etransclem3  42805  etransclem7  42809  etransclem10  42812  etransclem21  42823  lincext1  44789
  Copyright terms: Public domain W3C validator