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

Theorem ifbid 4057
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 4056 . 2 ((𝜓𝜒) → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  ifcif 4035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-if 4036
This theorem is referenced by:  ifbieq1d  4058  ifbieq2d  4060  ifbieq12d  4062  ifbieq12d2  4068  ifan  4083  ifor  4084  rabsnif  4201  suppsnop  7173  resixpfo  7809  pw2f1olem  7926  unxpdomlem1  8026  cantnflem1d  8445  cantnflem1  8446  dfac12lem1  8825  ttukeylem3  9193  2resupmax  11854  xaddval  11889  xmulcom  11927  xmulneg1  11930  repswswrd  13330  ccatco  13380  sgnval  13624  sumeq1  14215  sumsplit  14289  prodeq1f  14425  rpnnen2lem1  14730  rpnnen2lem2  14731  rpnnen2lem10  14739  sadadd2lem2  14958  sadfval  14960  sadcp1  14963  sadadd2lem  14967  sadcom  14971  pcmpt  15382  pcmpt2  15383  pcfac  15389  prmrec  15412  ramcl  15519  acsfn  16091  setcepi  16509  mgmnsgrpex  17189  sgrpnmndex  17190  frgpup3lem  17961  dpjrid  18232  abvtrivd  18611  psrlidm  19172  psrridm  19173  mvrval  19190  mvrval2  19191  mvrf1  19194  mplmonmul  19233  mplcoe1  19234  mplcoe3  19235  mplcoe5  19237  evlslem3  19283  coe1tm  19412  coe1tmfv2  19414  gsummoncoe1  19443  obsip  19831  uvcval  19890  uvcvval  19891  mat1comp  20012  mamulid  20013  mamurid  20014  mat1ov  20020  mattpos1  20028  mat1dimid  20046  scmateALT  20084  scmatscm  20085  1mavmul  20120  marrepval  20134  marrepeval  20135  marepvval  20139  ma1repveval  20143  1marepvmarrepid  20147  mdetdiagid  20172  mdetunilem8  20191  mdetunilem9  20192  maducoeval  20211  maducoeval2  20212  madutpos  20214  madugsum  20215  minmar1val  20220  minmar1eval  20221  symgmatr01lem  20225  symgmatr01  20226  gsummatr01lem3  20229  gsummatr01lem4  20230  gsummatr01  20231  m2cpm  20312  m2cpminvid2lem  20325  decpmatid  20341  monmatcollpw  20350  mp2pm2mplem4  20380  chmatval  20400  fvmptnn04if  20420  fclsval  21569  tmsxpsval2  22101  dscmet  22134  dscopn  22135  ovolicc1  23035  ovolicc  23042  i1f1lem  23206  itg11  23208  i1fpos  23223  itg2uba  23260  itg2split  23266  itg2monolem1  23267  itg2cnlem1  23278  itg2cnlem2  23279  itg2cn  23280  ibllem  23281  isibl  23282  itgeq1f  23288  itgresr  23295  iblpos  23309  itgposval  23312  i1fibl  23324  ibladdlem  23336  iblabslem  23344  itgcn  23359  coe1termlem  23762  coe1term  23763  cxpval  24154  leibpilem2  24412  leibpi  24413  prmorcht  24648  sqff1o  24652  pclogsum  24684  dchr1  24726  dchr2sum  24742  sum2dchr  24743  lgsval  24770  lgsneg  24790  lgsdilem  24793  lgsdir2  24799  lgsdir  24801  dchrisum0flblem2  24942  dchrisum0flb  24943  ostth1  25066  sgnsv  28851  sgnsval  28852  fzto1st  28977  psgnfzto1st  28979  smatfval  28982  1smat1  28991  indval  29196  indfval  29199  ddeval1  29417  ddeval0  29418  eulerpartlemgvv  29558  sgnneg  29722  signsvvfval  29774  signsvfn  29778  kur14  30245  mrsubrn  30457  finxpeq1  32182  poimirlem5  32367  poimirlem6  32368  poimirlem7  32369  poimirlem8  32370  poimirlem10  32372  poimirlem11  32373  poimirlem12  32374  poimirlem15  32377  poimirlem16  32378  poimirlem17  32379  poimirlem18  32380  poimirlem19  32381  poimirlem20  32382  poimirlem21  32383  poimirlem22  32384  poimirlem23  32385  poimirlem27  32389  itg2addnclem  32414  itg2gt0cn  32418  ibladdnclem  32419  iblabsnclem  32426  ftc1anclem5  32442  ftc1anc  32446  ftc2nc  32447  pw2f1ocnv  36405  flcidc  36546  refsum2cnlem1  38002  icccncfext  38556  fourierdlem112  38894  fourierswlem  38906  fouriersw  38907  etransclem1  38911  etransclem5  38915  etransclem17  38927  etransclem32  38942  etransclem41  38951  hoidmv1lelem2  39265  ovnhoi  39276  hspdifhsp  39289  hspmbl  39302  hoimbl  39304  ovnsubadd2  39319  suppmptcfin  41935  linc0scn0  41987  linc1  41989  lcoss  42000  el0ldep  42030
  Copyright terms: Public domain W3C validator