Theorem ifbid 3951

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 3950	. 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 1398   ifcif 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3930

This theorem is referenced by:  ifbieq1d  3952  ifbieq2d  3954  ifbieq12d  3956  ifan  3975  ifor  3976  rabsnif  4085  suppsnop  6905  resixpfo  7500  pw2f1olem  7614  unxpdomlem1  7717  cantnflem1d  8098  cantnflem1  8099  cantnflem1dOLD  8121  cantnflem1OLD  8122  dfac12lem1  8514  ttukeylem3  8882  xaddval  11425  xmulcom  11461  xmulneg1  11464  repswswrd  12747  ccatco  12792  sgnval  13003  sumeq1  13593  sumsplit  13665  prodeq1f  13797  rpnnen2lem1  14032  rpnnen2lem2  14033  rpnnen2lem10  14041  rpnnen  14044  sadadd2lem2  14184  sadfval  14186  sadcp1  14189  sadadd2lem  14193  sadcom  14197  pcmpt  14495  pcmpt2  14496  pcfac  14502  prmrec  14524  ramcl  14631  acsfn  15148  setcepi  15566  mgmnsgrpex  16248  sgrpnmndex  16249  frgpup3lem  16994  dpjrid  17306  abvtrivd  17684  psrlidm  18251  psrlidmOLD  18252  psrridm  18253  psrridmOLD  18254  mvrval  18272  mvrval2  18273  mvrf1  18276  mplmonmul  18321  mplcoe1  18322  mplcoe3  18323  mplcoe3OLD  18324  mplcoe5  18326  mplcoe2OLD  18328  evlslem3  18378  coe1tm  18509  coe1tmfv2  18511  gsummoncoe1  18541  obsip  18925  uvcval  18987  uvcvval  18988  mat1comp  19109  mamulid  19110  mamurid  19111  mat1ov  19117  mattpos1  19125  mat1dimid  19143  scmateALT  19181  scmatscm  19182  1mavmul  19217  marrepval  19231  marrepeval  19232  marepvval  19236  ma1repveval  19240  1marepvmarrepid  19244  mdetdiagid  19269  mdetunilem8  19288  mdetunilem9  19289  maducoeval  19308  maducoeval2  19309  madutpos  19311  madugsum  19312  minmar1val  19317  minmar1eval  19318  symgmatr01lem  19322  symgmatr01  19323  gsummatr01lem3  19326  gsummatr01lem4  19327  gsummatr01  19328  m2cpm  19409  m2cpminvid2lem  19422  decpmatid  19438  monmatcollpw  19447  mp2pm2mplem4  19477  chmatval  19497  fvmptnn04if  19517  fclsval  20675  tmsxpsval2  21208  dscmet  21259  dscopn  21260  ovolicc1  22093  ovolicc  22100  i1f1lem  22262  itg11  22264  i1fpos  22279  itg2uba  22316  itg2split  22322  itg2monolem1  22323  itg2cnlem1  22334  itg2cnlem2  22335  itg2cn  22336  ibllem  22337  isibl  22338  itgeq1f  22344  itgresr  22351  iblpos  22365  itgposval  22368  i1fibl  22380  ibladdlem  22392  iblabslem  22400  itgcn  22415  coe1termlem  22821  coe1term  22822  cxpval  23213  leibpilem2  23469  leibpi  23470  prmorcht  23650  sqff1o  23654  pclogsum  23688  dchr1  23730  dchr2sum  23746  sum2dchr  23747  lgsval  23773  lgsneg  23792  lgsdilem  23795  lgsdir2  23801  lgsdir  23803  dchrisum0flblem2  23892  dchrisum0flb  23893  ostth1  24016  sgnsv  27951  sgnsval  27952  indval  28243  indfval  28246  ddeval1  28443  ddeval0  28444  eulerpartlemgvv  28579  sgnneg  28743  signsvvfval  28799  signsvfn  28803  kur14  28924  mrsubrn  29137  itg2addnclem  30306  itg2gt0cn  30310  ibladdnclem  30311  iblabsnclem  30318  ftc1anclem5  30334  ftc1anc  30338  ftc2nc  30339  pw2f1ocnv  31218  flcidc  31364  refsum2cnlem1  31652  icccncfext  31929  fourierdlem112  32240  fourierswlem  32252  fouriersw  32253  etransclem1  32257  etransclem5  32261  etransclem17  32273  etransclem32  32288  etransclem41  32297  suppmptcfin  33226  linc0scn0  33278  linc1  33280  lcoss  33291  el0ldep  33321