Theorem ifbid 3816

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 3815	. 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 1369   ifcif 3796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-if 3797

This theorem is referenced by:  ifbieq1d  3817  ifbieq2d  3819  ifbieq12d  3821  ifan  3840  ifor  3841  rabsnif  3949  suppsnop  6709  resixpfo  7306  pw2f1olem  7420  unxpdomlem1  7522  cantnflem1d  7901  cantnflem1  7902  cantnflem1dOLD  7924  cantnflem1OLD  7925  dfac12lem1  8317  ttukeylem3  8685  xaddval  11198  xmulcom  11234  xmulneg1  11237  repswswrd  12427  ccatco  12468  sgnval  12582  sumeq1  13171  sumsplit  13240  rpnnen2lem1  13502  rpnnen2lem2  13503  rpnnen2lem10  13511  rpnnen  13514  sadadd2lem2  13651  sadfval  13653  sadcp1  13656  sadadd2lem  13660  sadcom  13664  pcmpt  13959  pcmpt2  13960  pcfac  13966  prmrec  13988  ramcl  14095  acsfn  14602  setcepi  14961  frgpup3lem  16279  dpjrid  16566  abvtrivd  16930  psrlidm  17479  psrlidmOLD  17480  psrridm  17481  psrridmOLD  17482  mvrval  17499  mvrval2  17500  mvrf1  17503  mplmonmul  17548  mplcoe1  17549  mplcoe3  17550  mplcoe3OLD  17551  mplcoe5  17553  mplcoe2OLD  17555  evlslem3  17605  coe1tm  17731  coe1tmfv2  17733  obsip  18151  uvcval  18215  uvcvval  18216  dmatcomp  18308  mamulid  18309  mamurid  18310  mat1ov  18340  mattpos1  18345  1mavmul  18364  marrepval  18378  marrepeval  18379  marepvval  18383  ma1repveval  18387  1marepvmarrepid  18391  mdetunilem8  18430  mdetunilem9  18431  maducoeval  18450  maducoeval2  18451  madutpos  18453  madugsum  18454  minmar1val  18459  minmar1eval  18460  symgmatr01lem  18464  symgmatr01  18465  gsummatr01lem3  18468  gsummatr01lem4  18469  gsummatr01  18470  fclsval  19586  tmsxpsval2  20119  dscmet  20170  dscopn  20171  ovolicc1  21004  ovolicc  21011  i1f1lem  21172  itg11  21174  i1fpos  21189  itg2uba  21226  itg2split  21232  itg2monolem1  21233  itg2cnlem1  21244  itg2cnlem2  21245  itg2cn  21246  ibllem  21247  isibl  21248  itgeq1f  21254  itgresr  21261  iblpos  21275  itgposval  21278  i1fibl  21290  ibladdlem  21302  iblabslem  21310  itgcn  21325  coe1termlem  21730  coe1term  21731  cxpval  22114  leibpilem2  22341  leibpi  22342  prmorcht  22521  sqff1o  22525  pclogsum  22559  dchr1  22601  dchr2sum  22617  sum2dchr  22618  lgsval  22644  lgsneg  22663  lgsdilem  22666  lgsdir2  22672  lgsdir  22674  dchrisum0flblem2  22763  dchrisum0flb  22764  ostth1  22887  sgnsv  26195  sgnsval  26196  indval  26475  indfval  26478  ddeval1  26655  ddeval0  26656  eulerpartlemgvv  26764  sgnneg  26928  signsvvfval  26984  signsvfn  26988  kur14  27109  prodeq1f  27426  itg2addnclem  28448  itg2gt0cn  28452  ibladdnclem  28453  iblabsnclem  28460  ftc1anclem5  28476  ftc1anc  28480  ftc2nc  28481  pw2f1ocnv  29391  flcidc  29536  refsum2cnlem1  29764  suppmptcfin  30798  gsummoncoe1  30848  mat1dimid  30875  pmatcollpw1id  30904  mp2pm2mplem4  30924  mdetdiagid  30942  linc0scn0  30962  linc1  30964  lcoss  30975  el0ldep  31005