Theorem ifbid 3963

Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005.)

Hypothesis

Ref	Expression
ifbid.1

Assertion

Ref	Expression
ifbid

Proof of Theorem ifbid

Step	Hyp	Ref	Expression
1		ifbid.1	. 2
2		ifbi 3962	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  ifcif 3941

This theorem is referenced by:  ifbieq1d  3964  ifbieq2d  3966  ifbieq12d  3968  ifan  3987  ifor  3988  rabsnif  4099  suppsnop  6932  resixpfo  7527  pw2f1olem  7641  unxpdomlem1  7744  cantnflem1d  8128  cantnflem1  8129  cantnflem1dOLD  8151  cantnflem1OLD  8152  dfac12lem1  8544  ttukeylem3  8912  xaddval  11451  xmulcom  11487  xmulneg1  11490  repswswrd  12756  ccatco  12801  sgnval  12921  sumeq1  13511  sumsplit  13583  prodeq1f  13715  rpnnen2lem1  13948  rpnnen2lem2  13949  rpnnen2lem10  13957  rpnnen  13960  sadadd2lem2  14100  sadfval  14102  sadcp1  14105  sadadd2lem  14109  sadcom  14113  pcmpt  14411  pcmpt2  14412  pcfac  14418  prmrec  14440  ramcl  14547  acsfn  15056  setcepi  15415  mgmnsgrpex  16049  sgrpnmndex  16050  frgpup3lem  16795  dpjrid  17111  abvtrivd  17489  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  mvrval  18077  mvrval2  18078  mvrf1  18081  mplmonmul  18126  mplcoe1  18127  mplcoe3  18128  mplcoe3OLD  18129  mplcoe5  18131  mplcoe2OLD  18133  evlslem3  18183  coe1tm  18314  coe1tmfv2  18316  gsummoncoe1  18346  obsip  18752  uvcval  18816  uvcvval  18817  mat1comp  18942  mamulid  18943  mamurid  18944  mat1ov  18950  mattpos1  18958  mat1dimid  18976  scmateALT  19014  scmatscm  19015  1mavmul  19050  marrepval  19064  marrepeval  19065  marepvval  19069  ma1repveval  19073  1marepvmarrepid  19077  mdetdiagid  19102  mdetunilem8  19121  mdetunilem9  19122  maducoeval  19141  maducoeval2  19142  madutpos  19144  madugsum  19145  minmar1val  19150  minmar1eval  19151  symgmatr01lem  19155  symgmatr01  19156  gsummatr01lem3  19159  gsummatr01lem4  19160  gsummatr01  19161  m2cpm  19242  m2cpminvid2lem  19255  decpmatid  19271  monmatcollpw  19280  mp2pm2mplem4  19310  chmatval  19330  fvmptnn04if  19350  fclsval  20509  tmsxpsval2  21042  dscmet  21093  dscopn  21094  ovolicc1  21927  ovolicc  21934  i1f1lem  22096  itg11  22098  i1fpos  22113  itg2uba  22150  itg2split  22156  itg2monolem1  22157  itg2cnlem1  22168  itg2cnlem2  22169  itg2cn  22170  ibllem  22171  isibl  22172  itgeq1f  22178  itgresr  22185  iblpos  22199  itgposval  22202  i1fibl  22214  ibladdlem  22226  iblabslem  22234  itgcn  22249  coe1termlem  22655  coe1term  22656  cxpval  23045  leibpilem2  23272  leibpi  23273  prmorcht  23452  sqff1o  23456  pclogsum  23490  dchr1  23532  dchr2sum  23548  sum2dchr  23549  lgsval  23575  lgsneg  23594  lgsdilem  23597  lgsdir2  23603  lgsdir  23605  dchrisum0flblem2  23694  dchrisum0flb  23695  ostth1  23818  sgnsv  27717  sgnsval  27718  indval  28027  indfval  28030  ddeval1  28206  ddeval0  28207  eulerpartlemgvv  28315  sgnneg  28479  signsvvfval  28535  signsvfn  28539  kur14  28660  mrsubrn  28873  itg2addnclem  30066  itg2gt0cn  30070  ibladdnclem  30071  iblabsnclem  30078  ftc1anclem5  30094  ftc1anc  30098  ftc2nc  30099  pw2f1ocnv  30979  flcidc  31123  refsum2cnlem1  31412  icccncfext  31690  fourierdlem112  32001  fourierswlem  32013  fouriersw  32014  etransclem1  32018  etransclem5  32022  etransclem17  32034  etransclem32  32049  etransclem41  32058  suppmptcfin  32972  linc0scn0  33024  linc1  33026  lcoss  33037  el0ldep  33067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-if 3942