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

Theorem ifclda 4097
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 4069 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 482 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifclda.1 . . 3 ((𝜑𝜓) → 𝐴𝐶)
42, 3eqeltrd 2704 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5 iffalse 4072 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 482 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifclda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
86, 7eqeltrd 2704 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
94, 8pm2.61dan 831 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384   = wceq 1480  wcel 1992  ifcif 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-if 4064
This theorem is referenced by:  unxpdomlem3  8111  acndom  8819  iunfictbso  8882  dfac12lem2  8911  ttukeylem6  9281  canthp1lem2  9420  xaddf  11997  xmulf  12042  ccatcl  13293  swrdcl  13352  ccatco  13513  lo1bdd2  14184  o1lo1  14197  sadadd2lem2  15091  sadcaddlem  15098  sadadd2lem  15100  sadadd3  15102  lcmfval  15253  iserodd  15459  prmreclem2  15540  prmreclem4  15542  prmreclem6  15544  prmrec  15545  vdwlem6  15609  mreexexd  16224  symgextf  17753  pmtrf  17791  cyggex2  18214  dprdfid  18332  dmdprdsplitlem  18352  cygznlem1  19829  cygznlem2a  19830  cygznlem3  19832  cygth  19834  fvmptnn04if  20568  chfacfisf  20573  chfacfisfcpmat  20574  ptpjpre2  21288  ptopn2  21292  ptpjopn  21320  iccpnfcnv  22646  xrhmeo  22648  cmetcaulem  22989  ovolunlem1a  23166  ovolunlem1  23167  ioorf  23242  mbfi1fseqlem3  23385  mbfi1flim  23391  itg2seq  23410  itg2splitlem  23416  itg2split  23417  iblss  23472  itgle  23477  itgeqa  23481  ibladdlem  23487  itgaddlem1  23490  iblabslem  23495  iblabs  23496  iblabsr  23497  iblmulc2  23498  itgmulc2lem1  23499  bddmulibl  23506  itggt0  23509  itgcn  23510  ellimc2  23542  limccnp  23556  limccnp2  23557  dvcobr  23610  lhop1  23676  elplyd  23857  coeeq2  23897  dvply1  23938  aalioulem3  23988  dvtaylp  24023  dvradcnv  24074  psercnlem1  24078  logcnlem2  24284  logcnlem3  24285  logcnlem4  24286  logtayllem  24300  logtayl  24301  cxpcl  24315  recxpcl  24316  leibpilem2  24563  leibpi  24564  rlimcnp2  24588  efrlim  24591  igamf  24672  igamcl  24673  pclogsum  24835  dchrelbasd  24859  lgsfcl2  24923  lgscllem  24924  lgsval2lem  24927  lgsne0  24955  dchrvmasumiflem2  25086  dchrisum0flblem1  25092  pntrlog2bndlem4  25164  pntrlog2bndlem5  25165  pntlemj  25187  padicabv  25214  crctcshwlkn0  26576  sgnsval  29505  xrge0iifcnv  29753  xrge0iifhom  29757  pnfneige0  29771  esumpinfval  29908  sigaclfu2  29957  ballotlemsv  30344  ballotlemsdom  30346  signswmnd  30406  signsvvf  30428  signsvfn  30431  mrsubcv  31107  mrsubff  31109  mrsubrn  31110  mrsubccat  31115  unblimceq0lem  32131  ptrecube  33027  poimirlem24  33051  itg2addnclem2  33080  itg2gt0cn  33083  ibladdnclem  33084  itgaddnclem1  33086  iblabsnclem  33091  iblabsnc  33092  iblmulc2nc  33093  itgmulc2nclem1  33094  bddiblnc  33098  itggt0cn  33100  ftc1anclem5  33107  ftc1anclem6  33108  ftc1anclem7  33109  ftc1anclem8  33110  ftc1anc  33111  areacirc  33123  cdleme27cl  35120  sdrgacs  37238  climsuse  39231  lptioo1  39255  icccncfext  39391  cncfiooicclem1  39397  iblsplit  39476  dirkerval2  39605  dirkerre  39606  fourierdlem9  39627  fourierdlem17  39635  fourierdlem43  39661  etransclem3  39748  etransclem7  39752  etransclem10  39755  etransclem21  39766  lincext1  41505
  Copyright terms: Public domain W3C validator