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

Theorem ifclda 4153
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 4125 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 481 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifclda.1 . . 3 ((𝜑𝜓) → 𝐴𝐶)
42, 3eqeltrd 2730 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
5 iffalse 4128 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 481 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifclda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵𝐶)
86, 7eqeltrd 2730 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
94, 8pm2.61dan 849 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383   = wceq 1523  wcel 2030  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120
This theorem is referenced by:  unxpdomlem3  8207  acndom  8912  iunfictbso  8975  dfac12lem2  9004  ttukeylem6  9374  canthp1lem2  9513  xaddf  12093  xmulf  12140  ccatcl  13392  swrdcl  13464  ccatco  13627  lo1bdd2  14299  o1lo1  14312  sadadd2lem2  15219  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  lcmfval  15381  iserodd  15587  prmreclem2  15668  prmreclem4  15670  prmreclem6  15672  prmrec  15673  vdwlem6  15737  mreexexd  16355  symgextf  17883  pmtrf  17921  cyggex2  18344  dprdfid  18462  dmdprdsplitlem  18482  cygznlem1  19963  cygznlem2a  19964  cygznlem3  19966  cygth  19968  fvmptnn04if  20702  chfacfisf  20707  chfacfisfcpmat  20708  ptpjpre2  21431  ptopn2  21435  ptpjopn  21463  iccpnfcnv  22790  xrhmeo  22792  cmetcaulem  23132  ovolunlem1a  23310  ovolunlem1  23311  ioorf  23387  mbfi1fseqlem3  23529  mbfi1flim  23535  itg2seq  23554  itg2splitlem  23560  itg2split  23561  iblss  23616  itgle  23621  itgeqa  23625  ibladdlem  23631  itgaddlem1  23634  iblabslem  23639  iblabs  23640  iblabsr  23641  iblmulc2  23642  itgmulc2lem1  23643  bddmulibl  23650  itggt0  23653  itgcn  23654  ellimc2  23686  limccnp  23700  limccnp2  23701  dvcobr  23754  lhop1  23822  elplyd  24003  coeeq2  24043  dvply1  24084  aalioulem3  24134  dvtaylp  24169  dvradcnv  24220  psercnlem1  24224  logcnlem2  24434  logcnlem3  24435  logcnlem4  24436  logtayllem  24450  logtayl  24451  cxpcl  24465  recxpcl  24466  leibpilem2  24713  leibpi  24714  rlimcnp2  24738  efrlim  24741  igamf  24822  igamcl  24823  pclogsum  24985  dchrelbasd  25009  lgsfcl2  25073  lgscllem  25074  lgsval2lem  25077  lgsne0  25105  dchrvmasumiflem2  25236  dchrisum0flblem1  25242  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntlemj  25337  padicabv  25364  crctcshwlkn0  26769  sgnsval  29856  xrge0iifcnv  30107  xrge0iifhom  30111  pnfneige0  30125  esumpinfval  30263  sigaclfu2  30312  ballotlemsv  30699  ballotlemsdom  30701  signswmnd  30762  signsvvf  30784  signsvfn  30787  mrsubcv  31533  mrsubff  31535  mrsubrn  31536  mrsubccat  31541  unblimceq0lem  32622  ptrecube  33539  poimirlem24  33563  itg2addnclem2  33592  itg2gt0cn  33595  ibladdnclem  33596  itgaddnclem1  33598  iblabsnclem  33603  iblabsnc  33604  iblmulc2nc  33605  itgmulc2nclem1  33606  bddiblnc  33610  itggt0cn  33612  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  areacirc  33635  cdleme27cl  35971  sdrgacs  38088  climsuse  40158  lptioo1  40182  icccncfext  40418  cncfiooicclem1  40424  iblsplit  40500  dirkerval2  40629  dirkerre  40630  fourierdlem9  40651  fourierdlem17  40659  fourierdlem43  40685  etransclem3  40772  etransclem7  40776  etransclem10  40779  etransclem21  40790  lincext1  42568
  Copyright terms: Public domain W3C validator