Theorem ifbieq1d 3964

Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.)

Hypotheses

Ref	Expression
ifbieq1d.1
ifbieq1d.2

Assertion

Ref	Expression
ifbieq1d

Proof of Theorem ifbieq1d

Step	Hyp	Ref	Expression
1		ifbieq1d.1	. . 3
2	1	ifbid 3963	. 2
3		ifbieq1d.2	. . 3
4	3	ifeq1d 3959	. 2
5	2, 4	eqtrd 2498	1

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

This theorem is referenced by:  opeq1  4217  opeq2  4218  oieq1  7958  oieq2  7959  cantnflem1d  8128  cantnflem1  8129  cantnflem1dOLD  8151  cantnflem1OLD  8152  iunfictbso  8516  ttukey2g  8917  bcval  12382  swrdval  12644  summolem2a  13537  zsum  13540  fsum  13542  sumss  13546  sumss2  13548  fsumcvg2  13549  fsumser  13552  isumless  13657  cbvprod  13722  prodmolem2a  13741  zprod  13744  fprod  13748  fprodntriv  13749  prodss  13754  rpnnen2lem1  13948  rpnnen  13960  sadadd2lem  14109  sadadd2  14110  pcmpt  14411  pcmptdvds  14413  prmreclem2  14435  prmreclem4  14437  prmreclem5  14438  prmreclem6  14439  prmrec  14440  ramub1lem2  14545  ramcl  14547  pmtrval  16476  pmtrdifellem3  16503  cyggenod2  16888  gsummpt1n0  16992  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  evlslem2  18180  coe1tmmul2fv  18319  coe1pwmulfv  18321  cyggic  18611  dmatmulcl  19002  scmatscmiddistr  19010  marrepval  19064  maducoeval  19141  maducoeval2  19142  minmar1val  19150  fclsval  20509  stdbdmetval  21017  stdbdxmet  21018  pcopt2  21523  cmetcaulem  21727  ovolicc2lem3  21930  ovolicc2lem4  21931  ovolicc2lem5  21932  mbfposb  22060  i1fres  22112  i1fposd  22114  mbfi1fseqlem2  22123  mbfi1fseq  22128  mbfi1flimlem  22129  mbfi1flim  22130  itg2splitlem  22155  itg2cnlem1  22168  itg2cn  22170  isibl  22172  isibl2  22173  iblitg  22175  dfitg  22176  cbvitg  22182  itgeq2  22184  itgvallem  22191  iblneg  22209  itgneg  22210  itgss3  22221  itgcn  22249  deg1suble  22508  elply2  22593  dgrsub  22669  aareccl  22722  vmaval  23387  prmorcht  23452  pclogsum  23490  dchrelbasd  23514  dchrptlem2  23540  bposlem5  23563  lgsfval  23576  lgsdir  23605  lgsdilem2  23606  lgsdi  23607  lgsne0  23608  rplogsumlem2  23670  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  ballotlemsval  28447  ballotlemieq  28455  mrsubfval  28868  mblfinlem2  30052  itg2addnclem  30066  ftc1anclem5  30094  ftc1anclem6  30095  dvnprodlem1  31743  fourierdlem86  31975  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  afveq12d  32218  cdlemk40  36643

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-nfc 2607  df-rab 2816  df-v 3111  df-un 3480  df-if 3942