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

Theorem ifbid 3939
Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)
Hypothesis
Ref Expression
ifbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
ifbid  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)

Proof of Theorem ifbid
StepHypRef Expression
1 ifbid.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 ifbi 3938 . 2  |-  ( ( ps  <->  ch )  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B ) )
31, 2syl 17 1  |-  ( ph  ->  if ( ps ,  A ,  B )  =  if ( ch ,  A ,  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1438   ifcif 3917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-clab 2409  df-cleq 2415  df-clel 2418  df-if 3918
This theorem is referenced by:  ifbieq1d  3940  ifbieq2d  3942  ifbieq12d  3944  ifan  3963  ifor  3964  rabsnif  4075  suppsnop  6945  resixpfo  7577  pw2f1olem  7691  unxpdomlem1  7791  cantnflem1d  8207  cantnflem1  8208  dfac12lem1  8586  ttukeylem3  8954  xaddval  11529  xmulcom  11565  xmulneg1  11568  repswswrd  12895  ccatco  12940  sgnval  13157  sumeq1  13760  sumsplit  13834  prodeq1f  13967  rpnnen2lem1  14272  rpnnen2lem2  14273  rpnnen2lem10  14281  rpnnen  14284  sadadd2lem2  14429  sadfval  14431  sadcp1  14434  sadadd2lem  14438  sadcom  14442  pcmpt  14842  pcmpt2  14843  pcfac  14849  prmrec  14871  ramcl  14992  acsfn  15570  setcepi  15988  mgmnsgrpex  16670  sgrpnmndex  16671  frgpup3lem  17432  dpjrid  17700  abvtrivd  18073  psrlidm  18632  psrridm  18633  mvrval  18650  mvrval2  18651  mvrf1  18654  mplmonmul  18693  mplcoe1  18694  mplcoe3  18695  mplcoe5  18697  evlslem3  18742  coe1tm  18871  coe1tmfv2  18873  gsummoncoe1  18903  obsip  19288  uvcval  19347  uvcvval  19348  mat1comp  19469  mamulid  19470  mamurid  19471  mat1ov  19477  mattpos1  19485  mat1dimid  19503  scmateALT  19541  scmatscm  19542  1mavmul  19577  marrepval  19591  marrepeval  19592  marepvval  19596  ma1repveval  19600  1marepvmarrepid  19604  mdetdiagid  19629  mdetunilem8  19648  mdetunilem9  19649  maducoeval  19668  maducoeval2  19669  madutpos  19671  madugsum  19672  minmar1val  19677  minmar1eval  19678  symgmatr01lem  19682  symgmatr01  19683  gsummatr01lem3  19686  gsummatr01lem4  19687  gsummatr01  19688  m2cpm  19769  m2cpminvid2lem  19782  decpmatid  19798  monmatcollpw  19807  mp2pm2mplem4  19837  chmatval  19857  fvmptnn04if  19877  fclsval  21027  tmsxpsval2  21558  dscmet  21591  dscopn  21592  ovolicc1  22473  ovolicc  22481  i1f1lem  22651  itg11  22653  i1fpos  22668  itg2uba  22705  itg2split  22711  itg2monolem1  22712  itg2cnlem1  22723  itg2cnlem2  22724  itg2cn  22725  ibllem  22726  isibl  22727  itgeq1f  22733  itgresr  22740  iblpos  22754  itgposval  22757  i1fibl  22769  ibladdlem  22781  iblabslem  22789  itgcn  22804  coe1termlem  23216  coe1term  23217  cxpval  23613  leibpilem2  23871  leibpi  23872  prmorcht  24109  sqff1o  24113  pclogsum  24147  dchr1  24189  dchr2sum  24205  sum2dchr  24206  lgsval  24232  lgsneg  24251  lgsdilem  24254  lgsdir2  24260  lgsdir  24262  dchrisum0flblem2  24351  dchrisum0flb  24352  ostth1  24475  sgnsv  28503  sgnsval  28504  fzto1st  28630  psgnfzto1st  28632  smatfval  28635  1smat1  28644  indval  28849  indfval  28852  ddeval1  29071  ddeval0  29072  eulerpartlemgvv  29223  sgnneg  29425  signsvvfval  29481  signsvfn  29485  kur14  29953  mrsubrn  30165  finxpeq1  31748  poimirlem5  31915  poimirlem6  31916  poimirlem7  31917  poimirlem8  31918  poimirlem10  31920  poimirlem11  31921  poimirlem12  31922  poimirlem15  31925  poimirlem16  31926  poimirlem17  31927  poimirlem18  31928  poimirlem19  31929  poimirlem20  31930  poimirlem21  31931  poimirlem22  31932  poimirlem23  31933  poimirlem27  31937  itg2addnclem  31963  itg2gt0cn  31967  ibladdnclem  31968  iblabsnclem  31975  ftc1anclem5  31991  ftc1anc  31995  ftc2nc  31996  pw2f1ocnv  35868  flcidc  36016  refsum2cnlem1  37337  icccncfext  37711  fourierdlem112  38028  fourierswlem  38040  fouriersw  38041  etransclem1  38046  etransclem5  38050  etransclem17  38062  etransclem32  38077  etransclem41  38086  hoidmv1lelem2  38324  ovnhoi  38335  suppmptcfin  39783  linc0scn0  39835  linc1  39837  lcoss  39848  el0ldep  39878
  Copyright terms: Public domain W3C validator