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

Theorem ifbid 4252
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 4251 . 2 ((𝜓𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1632  ifcif 4230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-if 4231
This theorem is referenced by:  ifbieq1d  4253  ifbieq2d  4255  ifbieq12d  4257  ifbieq12d2  4263  ifan  4278  ifor  4279  rabsnif  4402  suppsnop  7478  resixpfo  8114  pw2f1olem  8231  unxpdomlem1  8331  cantnflem1d  8760  cantnflem1  8761  dfac12lem1  9177  ttukeylem3  9545  2resupmax  12232  xaddval  12267  xmulcom  12309  xmulneg1  12312  repswswrd  13751  ccatco  13801  sgnval  14047  sumeq1  14638  sumsplit  14718  prodeq1f  14857  rpnnen2lem1  15162  rpnnen2lem2  15163  rpnnen2lem10  15171  sadadd2lem2  15394  sadfval  15396  sadcp1  15399  sadadd2lem  15403  sadcom  15407  pcmpt  15818  pcmpt2  15819  pcfac  15825  prmrec  15848  ramcl  15955  acsfn  16541  setcepi  16959  mgmnsgrpex  17639  sgrpnmndex  17640  frgpup3lem  18410  dpjrid  18681  abvtrivd  19062  psrlidm  19625  psrridm  19626  mvrval  19643  mvrval2  19644  mvrf1  19647  mplmonmul  19686  mplcoe1  19687  mplcoe3  19688  mplcoe5  19690  evlslem3  19736  coe1tm  19865  coe1tmfv2  19867  gsummoncoe1  19896  obsip  20287  uvcval  20346  uvcvval  20347  mat1comp  20468  mamulid  20469  mamurid  20470  mat1ov  20476  mattpos1  20484  mat1dimid  20502  scmateALT  20540  scmatscm  20541  1mavmul  20576  marrepval  20590  marrepeval  20591  marepvval  20595  ma1repveval  20599  1marepvmarrepid  20603  mdetdiagid  20628  mdetunilem8  20647  mdetunilem9  20648  maducoeval  20667  maducoeval2  20668  madutpos  20670  madugsum  20671  minmar1val  20676  minmar1eval  20677  symgmatr01lem  20681  symgmatr01  20682  gsummatr01lem3  20685  gsummatr01lem4  20686  gsummatr01  20687  m2cpm  20768  m2cpminvid2lem  20781  decpmatid  20797  monmatcollpw  20806  mp2pm2mplem4  20836  chmatval  20856  fvmptnn04if  20876  fclsval  22033  tmsxpsval2  22565  dscmet  22598  dscopn  22599  ovolicc1  23504  ovolicc  23511  i1f1lem  23675  itg11  23677  i1fpos  23692  itg2uba  23729  itg2split  23735  itg2monolem1  23736  itg2cnlem1  23747  itg2cnlem2  23748  itg2cn  23749  ibllem  23750  isibl  23751  itgeq1f  23757  itgresr  23764  iblpos  23778  itgposval  23781  i1fibl  23793  ibladdlem  23805  iblabslem  23813  itgcn  23828  coe1termlem  24233  coe1term  24234  cxpval  24630  leibpilem2  24888  leibpi  24889  prmorcht  25124  sqff1o  25128  pclogsum  25160  dchr1  25202  dchr2sum  25218  sum2dchr  25219  lgsval  25246  lgsneg  25266  lgsdilem  25269  lgsdir2  25275  lgsdir  25277  dchrisum0flblem2  25418  dchrisum0flb  25419  ostth1  25542  sgnsv  30057  sgnsval  30058  fzto1st  30183  psgnfzto1st  30185  smatfval  30191  1smat1  30200  indval  30405  indfval  30408  prodindf  30415  ddeval1  30627  ddeval0  30628  eulerpartlemgvv  30768  sgnneg  30932  signsvvfval  30985  signsvfn  30989  hashreprin  31028  circlemeth  31048  kur14  31526  mrsubrn  31738  finxpeq1  33552  poimirlem5  33745  poimirlem6  33746  poimirlem7  33747  poimirlem8  33748  poimirlem10  33750  poimirlem11  33751  poimirlem12  33752  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem18  33758  poimirlem19  33759  poimirlem20  33760  poimirlem21  33761  poimirlem22  33762  poimirlem23  33763  poimirlem27  33767  itg2addnclem  33792  itg2gt0cn  33796  ibladdnclem  33797  iblabsnclem  33804  ftc1anclem5  33820  ftc1anc  33824  ftc2nc  33825  pw2f1ocnv  38124  flcidc  38264  refsum2cnlem1  39713  icccncfext  40621  fourierdlem112  40956  fourierswlem  40968  fouriersw  40969  etransclem1  40973  etransclem5  40977  etransclem17  40989  etransclem32  41004  etransclem41  41013  hoidmv1lelem2  41330  ovnhoi  41341  hspdifhsp  41354  hspmbl  41367  hoimbl  41369  ovnsubadd2  41384  suppmptcfin  42688  linc0scn0  42740  linc1  42742  lcoss  42753  el0ldep  42783
  Copyright terms: Public domain W3C validator