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

Theorem ifclda 4196
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 4168 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 473 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifclda.1 . . 3 ((𝜑𝜓) → 𝐴𝐶)
42, 3eqeltrd 2771 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5 iffalse 4171 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 473 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifclda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
86, 7eqeltrd 2771 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
94, 8pm2.61dan 867 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1564  wcel 2071  ifcif 4162
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-clab 2679  df-cleq 2685  df-clel 2688  df-if 4163
This theorem is referenced by:  unxpdomlem3  8250  acndom  8955  iunfictbso  9018  dfac12lem2  9047  ttukeylem6  9417  canthp1lem2  9556  xaddf  12137  xmulf  12184  ccatcl  13435  swrdcl  13507  ccatco  13670  lo1bdd2  14343  o1lo1  14356  sadadd2lem2  15263  sadcaddlem  15270  sadadd2lem  15272  sadadd3  15274  lcmfval  15425  iserodd  15631  prmreclem2  15712  prmreclem4  15714  prmreclem6  15716  prmrec  15717  vdwlem6  15781  mreexexd  16399  symgextf  17926  pmtrf  17964  cyggex2  18387  dprdfid  18505  dmdprdsplitlem  18525  cygznlem1  20006  cygznlem2a  20007  cygznlem3  20009  cygth  20011  fvmptnn04if  20745  chfacfisf  20750  chfacfisfcpmat  20751  ptpjpre2  21474  ptopn2  21478  ptpjopn  21506  iccpnfcnv  22833  xrhmeo  22835  cmetcaulem  23175  ovolunlem1a  23353  ovolunlem1  23354  ioorf  23430  mbfi1fseqlem3  23572  mbfi1flim  23578  itg2seq  23597  itg2splitlem  23603  itg2split  23604  iblss  23659  itgle  23664  itgeqa  23668  ibladdlem  23674  itgaddlem1  23677  iblabslem  23682  iblabs  23683  iblabsr  23684  iblmulc2  23685  itgmulc2lem1  23686  bddmulibl  23693  itggt0  23696  itgcn  23697  ellimc2  23729  limccnp  23743  limccnp2  23744  dvcobr  23797  lhop1  23865  elplyd  24046  coeeq2  24086  dvply1  24127  aalioulem3  24177  dvtaylp  24212  dvradcnv  24263  psercnlem1  24267  logcnlem2  24477  logcnlem3  24478  logcnlem4  24479  logtayllem  24493  logtayl  24494  cxpcl  24508  recxpcl  24509  leibpilem2  24756  leibpi  24757  rlimcnp2  24781  efrlim  24784  igamf  24865  igamcl  24866  pclogsum  25028  dchrelbasd  25052  lgsfcl2  25116  lgscllem  25117  lgsval2lem  25120  lgsne0  25148  dchrvmasumiflem2  25279  dchrisum0flblem1  25285  pntrlog2bndlem4  25357  pntrlog2bndlem5  25358  pntlemj  25380  padicabv  25407  crctcshwlkn0  26813  sgnsval  29926  xrge0iifcnv  30177  xrge0iifhom  30181  pnfneige0  30195  esumpinfval  30333  sigaclfu2  30382  ballotlemsv  30769  ballotlemsdom  30771  signswmnd  30832  signsvvf  30854  signsvfn  30857  mrsubcv  31603  mrsubff  31605  mrsubrn  31606  mrsubccat  31611  unblimceq0lem  32692  ptrecube  33609  poimirlem24  33633  itg2addnclem2  33662  itg2gt0cn  33665  ibladdnclem  33666  itgaddnclem1  33668  iblabsnclem  33673  iblabsnc  33674  iblmulc2nc  33675  itgmulc2nclem1  33676  bddiblnc  33680  itggt0cn  33682  ftc1anclem5  33689  ftc1anclem6  33690  ftc1anclem7  33691  ftc1anclem8  33692  ftc1anc  33693  areacirc  33705  cdleme27cl  36041  sdrgacs  38158  climsuse  40228  lptioo1  40252  icccncfext  40488  cncfiooicclem1  40494  iblsplit  40570  dirkerval2  40699  dirkerre  40700  fourierdlem9  40721  fourierdlem17  40729  fourierdlem43  40755  etransclem3  40842  etransclem7  40846  etransclem10  40849  etransclem21  40860  lincext1  42638
  Copyright terms: Public domain W3C validator