Theorem ifbid 3961

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

Step	Hyp	Ref	Expression
1		ifbid.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		ifbi 3960	. 2 |- ( ( ps <-> ch ) -> if ( ps , A , B ) = if ( ch , A , B ) )
3	1, 2	syl 16	1 |- ( ph -> if ( ps , A , B ) = if ( ch , A , B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   ifcif 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940

This theorem is referenced by:  ifbieq1d  3962  ifbieq2d  3964  ifbieq12d  3966  ifan  3985  ifor  3986  rabsnif  4096  suppsnop  6912  resixpfo  7504  pw2f1olem  7618  unxpdomlem1  7721  cantnflem1d  8103  cantnflem1  8104  cantnflem1dOLD  8126  cantnflem1OLD  8127  dfac12lem1  8519  ttukeylem3  8887  xaddval  11418  xmulcom  11454  xmulneg1  11457  repswswrd  12715  ccatco  12760  sgnval  12880  sumeq1  13470  sumsplit  13542  rpnnen2lem1  13805  rpnnen2lem2  13806  rpnnen2lem10  13814  rpnnen  13817  sadadd2lem2  13955  sadfval  13957  sadcp1  13960  sadadd2lem  13964  sadcom  13968  pcmpt  14266  pcmpt2  14267  pcfac  14273  prmrec  14295  ramcl  14402  acsfn  14910  setcepi  15269  frgpup3lem  16591  dpjrid  16901  abvtrivd  17272  psrlidm  17827  psrlidmOLD  17828  psrridm  17829  psrridmOLD  17830  mvrval  17848  mvrval2  17849  mvrf1  17852  mplmonmul  17897  mplcoe1  17898  mplcoe3  17899  mplcoe3OLD  17900  mplcoe5  17902  mplcoe2OLD  17904  evlslem3  17954  coe1tm  18085  coe1tmfv2  18087  gsummoncoe1  18117  obsip  18519  uvcval  18583  uvcvval  18584  mat1comp  18709  mamulid  18710  mamurid  18711  mat1ov  18717  mattpos1  18725  mat1dimid  18743  scmateALT  18781  scmatscm  18782  1mavmul  18817  marrepval  18831  marrepeval  18832  marepvval  18836  ma1repveval  18840  1marepvmarrepid  18844  mdetdiagid  18869  mdetunilem8  18888  mdetunilem9  18889  maducoeval  18908  maducoeval2  18909  madutpos  18911  madugsum  18912  minmar1val  18917  minmar1eval  18918  symgmatr01lem  18922  symgmatr01  18923  gsummatr01lem3  18926  gsummatr01lem4  18927  gsummatr01  18928  m2cpm  19009  m2cpminvid2lem  19022  decpmatid  19038  monmatcollpw  19047  mp2pm2mplem4  19077  chmatval  19097  fvmptnn04if  19117  fclsval  20244  tmsxpsval2  20777  dscmet  20828  dscopn  20829  ovolicc1  21662  ovolicc  21669  i1f1lem  21831  itg11  21833  i1fpos  21848  itg2uba  21885  itg2split  21891  itg2monolem1  21892  itg2cnlem1  21903  itg2cnlem2  21904  itg2cn  21905  ibllem  21906  isibl  21907  itgeq1f  21913  itgresr  21920  iblpos  21934  itgposval  21937  i1fibl  21949  ibladdlem  21961  iblabslem  21969  itgcn  21984  coe1termlem  22389  coe1term  22390  cxpval  22773  leibpilem2  23000  leibpi  23001  prmorcht  23180  sqff1o  23184  pclogsum  23218  dchr1  23260  dchr2sum  23276  sum2dchr  23277  lgsval  23303  lgsneg  23322  lgsdilem  23325  lgsdir2  23331  lgsdir  23333  dchrisum0flblem2  23422  dchrisum0flb  23423  ostth1  23546  sgnsv  27379  sgnsval  27380  indval  27667  indfval  27670  ddeval1  27846  ddeval0  27847  eulerpartlemgvv  27955  sgnneg  28119  signsvvfval  28175  signsvfn  28179  kur14  28300  prodeq1f  28617  itg2addnclem  29643  itg2gt0cn  29647  ibladdnclem  29648  iblabsnclem  29655  ftc1anclem5  29671  ftc1anc  29675  ftc2nc  29676  pw2f1ocnv  30583  flcidc  30728  refsum2cnlem1  30990  icccncfext  31226  suppmptcfin  32045  linc0scn0  32097  linc1  32099  lcoss  32110  el0ldep  32140