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

Theorem ifbid 4472
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 4471 . 2 ((𝜓𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1538  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:  ifbieq1d  4473  ifbieq2d  4475  ifbieq12d  4477  ifbieq12d2  4483  ifan  4501  ifor  4502  rabsnif  4644  suppsnop  7840  resixpfo  8496  pw2f1olem  8617  unxpdomlem1  8719  cantnflem1d  9148  cantnflem1  9149  dfac12lem1  9567  ttukeylem3  9931  2resupmax  12578  xaddval  12613  xmulcom  12656  xmulneg1  12659  repswswrd  14146  ccatco  14197  sgnval  14447  sumeq1  15045  sumsplit  15123  prodeq1f  15262  rpnnen2lem1  15567  rpnnen2lem2  15568  rpnnen2lem10  15576  sadadd2lem2  15797  sadfval  15799  sadcp1  15802  sadadd2lem  15806  sadcom  15810  pcmpt  16226  pcmpt2  16227  pcfac  16233  prmrec  16256  ramcl  16363  acsfn  16930  setcepi  17348  mgmnsgrpex  18096  sgrpnmndex  18097  frgpup3lem  18903  dpjrid  19184  abvtrivd  19611  psrlidm  20183  psrridm  20184  mvrval  20201  mvrval2  20202  mvrf1  20205  mplmonmul  20245  mplcoe1  20246  mplcoe3  20247  mplcoe5  20249  evlslem3  20293  coe1tm  20441  coe1tmfv2  20443  gsummoncoe1  20472  obsip  20865  uvcval  20929  uvcvval  20930  mat1comp  21049  mamulid  21050  mamurid  21051  mat1ov  21057  mattpos1  21065  mat1dimid  21083  scmateALT  21121  scmatscm  21122  1mavmul  21157  marrepval  21171  marrepeval  21172  marepvval  21176  ma1repveval  21180  1marepvmarrepid  21184  mdetdiagid  21209  mdetunilem8  21228  mdetunilem9  21229  maducoeval  21248  maducoeval2  21249  madutpos  21251  madugsum  21252  minmar1val  21257  minmar1eval  21258  symgmatr01lem  21262  symgmatr01  21263  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  m2cpm  21349  m2cpminvid2lem  21362  decpmatid  21378  monmatcollpw  21387  mp2pm2mplem4  21417  chmatval  21437  fvmptnn04if  21457  fclsval  22616  tmsxpsval2  23149  dscmet  23182  dscopn  23183  ovolicc1  24123  ovolicc  24130  i1f1lem  24296  itg11  24298  i1fpos  24313  itg2uba  24350  itg2split  24356  itg2monolem1  24357  itg2cnlem1  24368  itg2cnlem2  24369  itg2cn  24370  ibllem  24371  isibl  24372  itgeq1f  24378  itgresr  24385  iblpos  24399  itgposval  24402  i1fibl  24414  ibladdlem  24426  iblabslem  24434  itgcn  24451  coe1termlem  24858  coe1term  24859  cxpval  25258  leibpilem2  25530  leibpi  25531  prmorcht  25766  sqff1o  25770  pclogsum  25802  dchr1  25844  dchr2sum  25860  sum2dchr  25861  lgsval  25888  lgsneg  25908  lgsdilem  25911  lgsdir2  25917  lgsdir  25919  dchrisum0flblem2  26096  dchrisum0flb  26097  ostth1  26220  mptprop  30445  fzto1st  30777  psgnfzto1st  30779  sgnsv  30834  sgnsval  30835  smatfval  31120  1smat1  31129  indval  31329  indfval  31332  prodindf  31339  ddeval1  31550  ddeval0  31551  eulerpartlemgvv  31691  sgnneg  31855  signsvvfval  31905  signsvfn  31909  hashreprin  31948  circlemeth  31968  kur14  32520  ex-sategoelel  32725  mrsubrn  32817  finxpeq1  34748  poimirlem5  35007  poimirlem6  35008  poimirlem7  35009  poimirlem8  35010  poimirlem10  35012  poimirlem11  35013  poimirlem12  35014  poimirlem15  35017  poimirlem16  35018  poimirlem17  35019  poimirlem18  35020  poimirlem19  35021  poimirlem20  35022  poimirlem21  35023  poimirlem22  35024  poimirlem23  35025  poimirlem27  35029  itg2addnclem  35053  itg2gt0cn  35057  ibladdnclem  35058  iblabsnclem  35065  ftc1anclem5  35079  ftc1anc  35083  ftc2nc  35084  metakunt11  39306  frlmvscadiccat  39373  pw2f1ocnv  39894  flcidc  40034  refsum2cnlem1  41586  icccncfext  42455  fourierdlem112  42786  fourierswlem  42798  fouriersw  42799  etransclem1  42803  etransclem5  42807  etransclem17  42819  etransclem32  42834  etransclem41  42843  hoidmv1lelem2  43157  ovnhoi  43168  hspdifhsp  43181  hspmbl  43194  hoimbl  43196  ovnsubadd2  43211  suppmptcfin  44707  linc0scn0  44758  linc1  44760  lcoss  44771  el0ldep  44801
  Copyright terms: Public domain W3C validator