Theorem ifbid 3915

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 3914	. 2 |- ( ( ps <-> ch ) -> if ( ps , A , B ) = if ( ch , A , B ) )
3	1, 2	syl 17	1 |- ( ph -> if ( ps , A , B ) = if ( ch , A , B ) )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1455   ifcif 3893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-if 3894

This theorem is referenced by:  ifbieq1d  3916  ifbieq2d  3918  ifbieq12d  3920  ifan  3939  ifor  3940  rabsnif  4054  suppsnop  6955  resixpfo  7586  pw2f1olem  7702  unxpdomlem1  7802  cantnflem1d  8219  cantnflem1  8220  dfac12lem1  8599  ttukeylem3  8967  xaddval  11545  xmulcom  11581  xmulneg1  11584  repswswrd  12924  ccatco  12969  sgnval  13200  sumeq1  13804  sumsplit  13878  prodeq1f  14011  rpnnen2lem1  14316  rpnnen2lem2  14317  rpnnen2lem10  14325  rpnnen  14328  sadadd2lem2  14473  sadfval  14475  sadcp1  14478  sadadd2lem  14482  sadcom  14486  pcmpt  14886  pcmpt2  14887  pcfac  14893  prmrec  14915  ramcl  15036  acsfn  15614  setcepi  16032  mgmnsgrpex  16714  sgrpnmndex  16715  frgpup3lem  17476  dpjrid  17744  abvtrivd  18117  psrlidm  18676  psrridm  18677  mvrval  18694  mvrval2  18695  mvrf1  18698  mplmonmul  18737  mplcoe1  18738  mplcoe3  18739  mplcoe5  18741  evlslem3  18786  coe1tm  18915  coe1tmfv2  18917  gsummoncoe1  18947  obsip  19333  uvcval  19392  uvcvval  19393  mat1comp  19514  mamulid  19515  mamurid  19516  mat1ov  19522  mattpos1  19530  mat1dimid  19548  scmateALT  19586  scmatscm  19587  1mavmul  19622  marrepval  19636  marrepeval  19637  marepvval  19641  ma1repveval  19645  1marepvmarrepid  19649  mdetdiagid  19674  mdetunilem8  19693  mdetunilem9  19694  maducoeval  19713  maducoeval2  19714  madutpos  19716  madugsum  19717  minmar1val  19722  minmar1eval  19723  symgmatr01lem  19727  symgmatr01  19728  gsummatr01lem3  19731  gsummatr01lem4  19732  gsummatr01  19733  m2cpm  19814  m2cpminvid2lem  19827  decpmatid  19843  monmatcollpw  19852  mp2pm2mplem4  19882  chmatval  19902  fvmptnn04if  19922  fclsval  21072  tmsxpsval2  21603  dscmet  21636  dscopn  21637  ovolicc1  22518  ovolicc  22526  i1f1lem  22696  itg11  22698  i1fpos  22713  itg2uba  22750  itg2split  22756  itg2monolem1  22757  itg2cnlem1  22768  itg2cnlem2  22769  itg2cn  22770  ibllem  22771  isibl  22772  itgeq1f  22778  itgresr  22785  iblpos  22799  itgposval  22802  i1fibl  22814  ibladdlem  22826  iblabslem  22834  itgcn  22849  coe1termlem  23261  coe1term  23262  cxpval  23658  leibpilem2  23916  leibpi  23917  prmorcht  24154  sqff1o  24158  pclogsum  24192  dchr1  24234  dchr2sum  24250  sum2dchr  24251  lgsval  24277  lgsneg  24296  lgsdilem  24299  lgsdir2  24305  lgsdir  24307  dchrisum0flblem2  24396  dchrisum0flb  24397  ostth1  24520  sgnsv  28539  sgnsval  28540  fzto1st  28665  psgnfzto1st  28667  smatfval  28670  1smat1  28679  indval  28884  indfval  28887  ddeval1  29106  ddeval0  29107  eulerpartlemgvv  29258  sgnneg  29460  signsvvfval  29516  signsvfn  29520  kur14  29988  mrsubrn  30200  finxpeq1  31823  poimirlem5  31990  poimirlem6  31991  poimirlem7  31992  poimirlem8  31993  poimirlem10  31995  poimirlem11  31996  poimirlem12  31997  poimirlem15  32000  poimirlem16  32001  poimirlem17  32002  poimirlem18  32003  poimirlem19  32004  poimirlem20  32005  poimirlem21  32006  poimirlem22  32007  poimirlem23  32008  poimirlem27  32012  itg2addnclem  32038  itg2gt0cn  32042  ibladdnclem  32043  iblabsnclem  32050  ftc1anclem5  32066  ftc1anc  32070  ftc2nc  32071  pw2f1ocnv  35937  flcidc  36085  refsum2cnlem1  37398  icccncfext  37803  fourierdlem112  38120  fourierswlem  38132  fouriersw  38133  etransclem1  38138  etransclem5  38142  etransclem17  38154  etransclem32  38169  etransclem41  38178  hoidmv1lelem2  38452  ovnhoi  38463  hspdifhsp  38476  hspmbl  38489  hoimbl  38491  suppmptcfin  40437  linc0scn0  40489  linc1  40491  lcoss  40502  el0ldep  40532