Theorem ifbid 3808

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 3807	. 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 1364   ifcif 3788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-if 3789

This theorem is referenced by:  ifbieq1d  3809  ifbieq2d  3811  ifbieq12d  3813  ifan  3832  ifor  3833  rabsnif  3941  suppsnop  6703  resixpfo  7297  pw2f1olem  7411  unxpdomlem1  7513  cantnflem1d  7892  cantnflem1  7893  cantnflem1dOLD  7915  cantnflem1OLD  7916  dfac12lem1  8308  ttukeylem3  8676  xaddval  11189  xmulcom  11225  xmulneg1  11228  repswswrd  12418  ccatco  12459  sgnval  12573  sumeq1  13162  sumsplit  13231  rpnnen2lem1  13493  rpnnen2lem2  13494  rpnnen2lem10  13502  rpnnen  13505  sadadd2lem2  13642  sadfval  13644  sadcp1  13647  sadadd2lem  13651  sadcom  13655  pcmpt  13950  pcmpt2  13951  pcfac  13957  prmrec  13979  ramcl  14086  acsfn  14593  setcepi  14952  frgpup3lem  16267  dpjrid  16551  abvtrivd  16905  psrlidm  17452  psrlidmOLD  17453  psrridm  17454  psrridmOLD  17455  mvrval  17472  mvrval2  17473  mvrf1  17476  mplmonmul  17521  mplcoe1  17522  mplcoe3  17523  mplcoe3OLD  17524  mplcoe2  17525  mplcoe2OLD  17526  evlslem3  17576  coe1tm  17701  coe1tmfv2  17703  obsip  18105  uvcval  18169  uvcvval  18170  dmatcomp  18262  mamulid  18263  mamurid  18264  mat1ov  18294  mattpos1  18299  1mavmul  18318  marrepval  18332  marrepeval  18333  marepvval  18337  ma1repveval  18341  1marepvmarrepid  18345  mdetunilem8  18384  mdetunilem9  18385  maducoeval  18404  maducoeval2  18405  madutpos  18407  madugsum  18408  minmar1val  18413  minmar1eval  18414  symgmatr01lem  18418  symgmatr01  18419  gsummatr01lem3  18422  gsummatr01lem4  18423  gsummatr01  18424  fclsval  19540  tmsxpsval2  20073  dscmet  20124  dscopn  20125  ovolicc1  20958  ovolicc  20965  i1f1lem  21126  itg11  21128  i1fpos  21143  itg2uba  21180  itg2split  21186  itg2monolem1  21187  itg2cnlem1  21198  itg2cnlem2  21199  itg2cn  21200  ibllem  21201  isibl  21202  itgeq1f  21208  itgresr  21215  iblpos  21229  itgposval  21232  i1fibl  21244  ibladdlem  21256  iblabslem  21264  itgcn  21279  coe1termlem  21684  coe1term  21685  cxpval  22068  leibpilem2  22295  leibpi  22296  prmorcht  22475  sqff1o  22479  pclogsum  22513  dchr1  22555  dchr2sum  22571  sum2dchr  22572  lgsval  22598  lgsneg  22617  lgsdilem  22620  lgsdir2  22626  lgsdir  22628  dchrisum0flblem2  22717  dchrisum0flb  22718  ostth1  22841  sgnsv  26123  sgnsval  26124  indval  26406  indfval  26409  ddeval1  26586  ddeval0  26587  eulerpartlemgvv  26689  sgnneg  26853  signsvvfval  26909  signsvfn  26913  kur14  27034  prodeq1f  27350  itg2addnclem  28368  itg2gt0cn  28372  ibladdnclem  28373  iblabsnclem  28380  ftc1anclem5  28396  ftc1anc  28400  ftc2nc  28401  pw2f1ocnv  29311  flcidc  29456  refsum2cnlem1  29684  suppmptcfin  30709  mat1dimid  30753  mdetdiagid  30778  linc0scn0  30798  linc1  30800  lcoss  30811  el0ldep  30841