Theorem ifbid 3937

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 3936	. 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 187   = wceq 1437   ifcif 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-if 3916

This theorem is referenced by:  ifbieq1d  3938  ifbieq2d  3940  ifbieq12d  3942  ifan  3961  ifor  3962  rabsnif  4072  suppsnop  6939  resixpfo  7568  pw2f1olem  7682  unxpdomlem1  7782  cantnflem1d  8192  cantnflem1  8193  dfac12lem1  8571  ttukeylem3  8939  xaddval  11516  xmulcom  11552  xmulneg1  11555  repswswrd  12872  ccatco  12917  sgnval  13130  sumeq1  13733  sumsplit  13807  prodeq1f  13940  rpnnen2lem1  14245  rpnnen2lem2  14246  rpnnen2lem10  14254  rpnnen  14257  sadadd2lem2  14398  sadfval  14400  sadcp1  14403  sadadd2lem  14407  sadcom  14411  pcmpt  14800  pcmpt2  14801  pcfac  14807  prmrec  14829  ramcl  14950  acsfn  15516  setcepi  15934  mgmnsgrpex  16616  sgrpnmndex  16617  frgpup3lem  17362  dpjrid  17630  abvtrivd  18003  psrlidm  18562  psrridm  18563  mvrval  18580  mvrval2  18581  mvrf1  18584  mplmonmul  18623  mplcoe1  18624  mplcoe3  18625  mplcoe5  18627  evlslem3  18672  coe1tm  18801  coe1tmfv2  18803  gsummoncoe1  18833  obsip  19215  uvcval  19274  uvcvval  19275  mat1comp  19396  mamulid  19397  mamurid  19398  mat1ov  19404  mattpos1  19412  mat1dimid  19430  scmateALT  19468  scmatscm  19469  1mavmul  19504  marrepval  19518  marrepeval  19519  marepvval  19523  ma1repveval  19527  1marepvmarrepid  19531  mdetdiagid  19556  mdetunilem8  19575  mdetunilem9  19576  maducoeval  19595  maducoeval2  19596  madutpos  19598  madugsum  19599  minmar1val  19604  minmar1eval  19605  symgmatr01lem  19609  symgmatr01  19610  gsummatr01lem3  19613  gsummatr01lem4  19614  gsummatr01  19615  m2cpm  19696  m2cpminvid2lem  19709  decpmatid  19725  monmatcollpw  19734  mp2pm2mplem4  19764  chmatval  19784  fvmptnn04if  19804  fclsval  20954  tmsxpsval2  21485  dscmet  21518  dscopn  21519  ovolicc1  22347  ovolicc  22354  i1f1lem  22524  itg11  22526  i1fpos  22541  itg2uba  22578  itg2split  22584  itg2monolem1  22585  itg2cnlem1  22596  itg2cnlem2  22597  itg2cn  22598  ibllem  22599  isibl  22600  itgeq1f  22606  itgresr  22613  iblpos  22627  itgposval  22630  i1fibl  22642  ibladdlem  22654  iblabslem  22662  itgcn  22677  coe1termlem  23080  coe1term  23081  cxpval  23474  leibpilem2  23732  leibpi  23733  prmorcht  23968  sqff1o  23972  pclogsum  24006  dchr1  24048  dchr2sum  24064  sum2dchr  24065  lgsval  24091  lgsneg  24110  lgsdilem  24113  lgsdir2  24119  lgsdir  24121  dchrisum0flblem2  24210  dchrisum0flb  24211  ostth1  24334  sgnsv  28328  sgnsval  28329  fzto1st  28455  psgnfzto1st  28457  smatfval  28460  1smat1  28469  indval  28674  indfval  28677  ddeval1  28896  ddeval0  28897  eulerpartlemgvv  29035  sgnneg  29199  signsvvfval  29255  signsvfn  29259  kur14  29727  mrsubrn  29939  poimirlem5  31649  poimirlem6  31650  poimirlem7  31651  poimirlem8  31652  poimirlem10  31654  poimirlem11  31655  poimirlem12  31656  poimirlem15  31659  poimirlem16  31660  poimirlem17  31661  poimirlem18  31662  poimirlem19  31663  poimirlem20  31664  poimirlem21  31665  poimirlem22  31666  poimirlem23  31667  poimirlem27  31671  itg2addnclem  31697  itg2gt0cn  31701  ibladdnclem  31702  iblabsnclem  31709  ftc1anclem5  31725  ftc1anc  31729  ftc2nc  31730  pw2f1ocnv  35598  flcidc  35739  refsum2cnlem1  36998  icccncfext  37337  fourierdlem112  37650  fourierswlem  37662  fouriersw  37663  etransclem1  37667  etransclem5  37671  etransclem17  37683  etransclem32  37698  etransclem41  37707  suppmptcfin  38933  linc0scn0  38985  linc1  38987  lcoss  38998  el0ldep  39028