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

Theorem ifbid 4141
Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)
Hypothesis
Ref Expression
ifbid.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
ifbid (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))

Proof of Theorem ifbid
StepHypRef Expression
1 ifbid.1 . 2 (𝜑 → (𝜓𝜒))
2 ifbi 4140 . 2 ((𝜓𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  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:  ifbieq1d  4142  ifbieq2d  4144  ifbieq12d  4146  ifbieq12d2  4152  ifan  4167  ifor  4168  rabsnif  4290  suppsnop  7354  resixpfo  7988  pw2f1olem  8105  unxpdomlem1  8205  cantnflem1d  8623  cantnflem1  8624  dfac12lem1  9003  ttukeylem3  9371  2resupmax  12057  xaddval  12092  xmulcom  12134  xmulneg1  12137  repswswrd  13577  ccatco  13627  sgnval  13872  sumeq1  14463  sumsplit  14543  prodeq1f  14682  rpnnen2lem1  14987  rpnnen2lem2  14988  rpnnen2lem10  14996  sadadd2lem2  15219  sadfval  15221  sadcp1  15224  sadadd2lem  15228  sadcom  15232  pcmpt  15643  pcmpt2  15644  pcfac  15650  prmrec  15673  ramcl  15780  acsfn  16367  setcepi  16785  mgmnsgrpex  17465  sgrpnmndex  17466  frgpup3lem  18236  dpjrid  18507  abvtrivd  18888  psrlidm  19451  psrridm  19452  mvrval  19469  mvrval2  19470  mvrf1  19473  mplmonmul  19512  mplcoe1  19513  mplcoe3  19514  mplcoe5  19516  evlslem3  19562  coe1tm  19691  coe1tmfv2  19693  gsummoncoe1  19722  obsip  20113  uvcval  20172  uvcvval  20173  mat1comp  20294  mamulid  20295  mamurid  20296  mat1ov  20302  mattpos1  20310  mat1dimid  20328  scmateALT  20366  scmatscm  20367  1mavmul  20402  marrepval  20416  marrepeval  20417  marepvval  20421  ma1repveval  20425  1marepvmarrepid  20429  mdetdiagid  20454  mdetunilem8  20473  mdetunilem9  20474  maducoeval  20493  maducoeval2  20494  madutpos  20496  madugsum  20497  minmar1val  20502  minmar1eval  20503  symgmatr01lem  20507  symgmatr01  20508  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  m2cpm  20594  m2cpminvid2lem  20607  decpmatid  20623  monmatcollpw  20632  mp2pm2mplem4  20662  chmatval  20682  fvmptnn04if  20702  fclsval  21859  tmsxpsval2  22391  dscmet  22424  dscopn  22425  ovolicc1  23330  ovolicc  23337  i1f1lem  23501  itg11  23503  i1fpos  23518  itg2uba  23555  itg2split  23561  itg2monolem1  23562  itg2cnlem1  23573  itg2cnlem2  23574  itg2cn  23575  ibllem  23576  isibl  23577  itgeq1f  23583  itgresr  23590  iblpos  23604  itgposval  23607  i1fibl  23619  ibladdlem  23631  iblabslem  23639  itgcn  23654  coe1termlem  24059  coe1term  24060  cxpval  24455  leibpilem2  24713  leibpi  24714  prmorcht  24949  sqff1o  24953  pclogsum  24985  dchr1  25027  dchr2sum  25043  sum2dchr  25044  lgsval  25071  lgsneg  25091  lgsdilem  25094  lgsdir2  25100  lgsdir  25102  dchrisum0flblem2  25243  dchrisum0flb  25244  ostth1  25367  sgnsv  29855  sgnsval  29856  fzto1st  29981  psgnfzto1st  29983  smatfval  29989  1smat1  29998  indval  30203  indfval  30206  prodindf  30213  ddeval1  30425  ddeval0  30426  eulerpartlemgvv  30566  sgnneg  30730  signsvvfval  30783  signsvfn  30787  hashreprin  30826  circlemeth  30846  kur14  31324  mrsubrn  31536  finxpeq1  33353  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem15  33554  poimirlem16  33555  poimirlem17  33556  poimirlem18  33557  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem27  33566  itg2addnclem  33591  itg2gt0cn  33595  ibladdnclem  33596  iblabsnclem  33603  ftc1anclem5  33619  ftc1anc  33623  ftc2nc  33624  pw2f1ocnv  37921  flcidc  38061  refsum2cnlem1  39510  icccncfext  40418  fourierdlem112  40753  fourierswlem  40765  fouriersw  40766  etransclem1  40770  etransclem5  40774  etransclem17  40786  etransclem32  40801  etransclem41  40810  hoidmv1lelem2  41127  ovnhoi  41138  hspdifhsp  41151  hspmbl  41164  hoimbl  41166  ovnsubadd2  41181  suppmptcfin  42485  linc0scn0  42537  linc1  42539  lcoss  42550  el0ldep  42580
  Copyright terms: Public domain W3C validator