Theorem ifbid 3717

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 3716	. 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 177   = wceq 1649   ifcif 3699

This theorem is referenced by:  ifbieq2d  3719  ifbieq12d  3721  ifan  3738  ifor  3739  riotabidva  6525  resixpfo  7059  pw2f1olem  7171  unxpdomlem1  7272  cantnflem1d  7600  cantnflem1  7601  dfac12lem1  7979  ttukeylem3  8347  xaddval  10765  xmulcom  10801  xmulneg1  10804  ccatco  11759  sumeq1f  12437  sumsplit  12507  rpnnen2lem1  12769  rpnnen2lem2  12770  rpnnen2lem10  12778  rpnnen  12781  sadadd2lem2  12917  sadfval  12919  sadcp1  12922  sadadd2lem  12926  sadcom  12930  pcmpt  13216  pcmpt2  13217  pcfac  13223  prmrec  13245  ramcl  13352  acsfn  13839  setcepi  14198  frgpup3lem  15364  dpjrid  15575  abvtrivd  15883  psrlidm  16422  psrridm  16423  mvrval  16440  mvrval2  16441  mvrf1  16444  mplmonmul  16482  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  coe1tm  16620  coe1tmfv2  16622  obsip  16903  fclsval  17993  tmsxpsval2  18522  dscmet  18573  dscopn  18574  ovolicc1  19365  ovolicc  19372  i1f1lem  19534  itg11  19536  i1fpos  19551  itg2uba  19588  itg2split  19594  itg2monolem1  19595  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  ibllem  19609  isibl  19610  itgeq1f  19616  itgresr  19623  iblpos  19637  itgposval  19640  i1fibl  19652  ibladdlem  19664  iblabslem  19672  itgcn  19687  evlslem3  19888  coe1termlem  20129  coe1term  20130  cxpval  20508  leibpilem2  20734  leibpi  20735  prmorcht  20914  sqff1o  20918  pclogsum  20952  dchr1  20994  dchr2sum  21010  sum2dchr  21011  lgsval  21037  lgsneg  21056  lgsdilem  21059  lgsdir2  21065  lgsdir  21067  dchrisum0flblem2  21156  dchrisum0flb  21157  ostth1  21280  indval  24364  indfval  24367  kur14  24855  prodeq1f  25187  itg2addnclem  26155  itg2gt0cn  26159  ibladdnclem  26160  iblabsnclem  26167  pw2f1ocnv  26998  uvcval  27102  uvcvval  27103  flcidc  27247  mamulid  27326  mamurid  27327  refsum2cnlem1  27575  sgnval  28232

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-if 3700