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

Theorem ifbid 4058
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 4057 . 2 ((𝜓𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195   = wceq 1475  ifcif 4036
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037
This theorem is referenced by:  ifbieq1d  4059  ifbieq2d  4061  ifbieq12d  4063  ifbieq12d2  4069  ifan  4084  ifor  4085  rabsnif  4202  suppsnop  7196  resixpfo  7832  pw2f1olem  7949  unxpdomlem1  8049  cantnflem1d  8468  cantnflem1  8469  dfac12lem1  8848  ttukeylem3  9216  2resupmax  11893  xaddval  11928  xmulcom  11968  xmulneg1  11971  repswswrd  13382  ccatco  13432  sgnval  13676  sumeq1  14267  sumsplit  14341  prodeq1f  14477  rpnnen2lem1  14782  rpnnen2lem2  14783  rpnnen2lem10  14791  sadadd2lem2  15010  sadfval  15012  sadcp1  15015  sadadd2lem  15019  sadcom  15023  pcmpt  15434  pcmpt2  15435  pcfac  15441  prmrec  15464  ramcl  15571  acsfn  16143  setcepi  16561  mgmnsgrpex  17241  sgrpnmndex  17242  frgpup3lem  18013  dpjrid  18284  abvtrivd  18663  psrlidm  19224  psrridm  19225  mvrval  19242  mvrval2  19243  mvrf1  19246  mplmonmul  19285  mplcoe1  19286  mplcoe3  19287  mplcoe5  19289  evlslem3  19335  coe1tm  19464  coe1tmfv2  19466  gsummoncoe1  19495  obsip  19884  uvcval  19943  uvcvval  19944  mat1comp  20065  mamulid  20066  mamurid  20067  mat1ov  20073  mattpos1  20081  mat1dimid  20099  scmateALT  20137  scmatscm  20138  1mavmul  20173  marrepval  20187  marrepeval  20188  marepvval  20192  ma1repveval  20196  1marepvmarrepid  20200  mdetdiagid  20225  mdetunilem8  20244  mdetunilem9  20245  maducoeval  20264  maducoeval2  20265  madutpos  20267  madugsum  20268  minmar1val  20273  minmar1eval  20274  symgmatr01lem  20278  symgmatr01  20279  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  m2cpm  20365  m2cpminvid2lem  20378  decpmatid  20394  monmatcollpw  20403  mp2pm2mplem4  20433  chmatval  20453  fvmptnn04if  20473  fclsval  21622  tmsxpsval2  22154  dscmet  22187  dscopn  22188  ovolicc1  23091  ovolicc  23098  i1f1lem  23262  itg11  23264  i1fpos  23279  itg2uba  23316  itg2split  23322  itg2monolem1  23323  itg2cnlem1  23334  itg2cnlem2  23335  itg2cn  23336  ibllem  23337  isibl  23338  itgeq1f  23344  itgresr  23351  iblpos  23365  itgposval  23368  i1fibl  23380  ibladdlem  23392  iblabslem  23400  itgcn  23415  coe1termlem  23818  coe1term  23819  cxpval  24210  leibpilem2  24468  leibpi  24469  prmorcht  24704  sqff1o  24708  pclogsum  24740  dchr1  24782  dchr2sum  24798  sum2dchr  24799  lgsval  24826  lgsneg  24846  lgsdilem  24849  lgsdir2  24855  lgsdir  24857  dchrisum0flblem2  24998  dchrisum0flb  24999  ostth1  25122  sgnsv  29058  sgnsval  29059  fzto1st  29184  psgnfzto1st  29186  smatfval  29189  1smat1  29198  indval  29403  indfval  29406  ddeval1  29624  ddeval0  29625  eulerpartlemgvv  29765  sgnneg  29929  signsvvfval  29981  signsvfn  29985  kur14  30452  mrsubrn  30664  finxpeq1  32399  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem27  32606  itg2addnclem  32631  itg2gt0cn  32635  ibladdnclem  32636  iblabsnclem  32643  ftc1anclem5  32659  ftc1anc  32663  ftc2nc  32664  pw2f1ocnv  36622  flcidc  36763  refsum2cnlem1  38219  icccncfext  38773  fourierdlem112  39111  fourierswlem  39123  fouriersw  39124  etransclem1  39128  etransclem5  39132  etransclem17  39144  etransclem32  39159  etransclem41  39168  hoidmv1lelem2  39482  ovnhoi  39493  hspdifhsp  39506  hspmbl  39519  hoimbl  39521  ovnsubadd2  39536  suppmptcfin  41954  linc0scn0  42006  linc1  42008  lcoss  42019  el0ldep  42049
  Copyright terms: Public domain W3C validator