Theorem ifbieq2d 3966

Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypotheses

Ref	Expression
ifbieq2d.1
ifbieq2d.2

Assertion

Ref	Expression
ifbieq2d

Proof of Theorem ifbieq2d

Step	Hyp	Ref	Expression
1		ifbieq2d.1	. . 3
2	1	ifbid 3963	. 2
3		ifbieq2d.2	. . 3
4	3	ifeq2d 3960	. 2
5	2, 4	eqtrd 2498	1

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

This theorem is referenced by:  tz7.44-2  7092  tz7.44-3  7093  oev  7183  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  fin23lem12  8732  fin23lem33  8746  axcc2  8838  ttukeylem3  8912  ttukey2g  8917  canthp1lem2  9052  canthp1  9053  xnegeq  11435  xaddval  11451  xmulval  11453  expval  12168  cshfn  12761  sgnval  12921  sadcp1  14105  smupp1  14130  gcdval  14146  gcdass  14183  iserodd  14359  pcval  14368  vdwlem6  14504  ramub1lem2  14545  ramcl  14547  mulgval  16144  symgextfv  16443  symgfixfo  16464  odval  16558  submod  16589  gexval  16598  znval  18572  fvmptnn04if  19350  cpmadumatpoly  19384  cayleyhamilton  19391  cayleyhamiltonALT  19392  ptcmplem2  20553  iccpnfhmeo  21445  pcopt  21522  ioombl1  21972  ioorval  21983  uniioombllem6  21997  itg1addlem3  22105  itg2uba  22150  limcfval  22276  limcmpt  22287  limcco  22297  dvcobr  22349  ig1pval  22573  abelthlem9  22835  logtayllem  23040  logtayl  23041  leibpilem2  23272  rlimcnp2  23296  efrlim  23299  muval  23406  lgsval  23575  lgsfval  23576  lgsval2lem  23581  rpvmasum2  23697  padicval  23802  padicabv  23815  axlowdimlem15  24259  axlowdim  24264  eupath2lem3  24979  eupath2  24980  gxval  25260  sgnsv  27717  sgnsval  27718  xrge0iifcv  27916  xrge0iifhom  27919  xrge0tmdOLD  27927  xrge0tmd  27928  ofccat  28497  signspval  28509  igamval  28589  rdgprc0  29226  dfrdg2  29228  dfrdg4  29600  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  fdc  30238  heiborlem4  30310  heiborlem6  30312  heiborlem10  30316  irrapxlem4  30761  lcmval  31198  lcmass  31218  dirkerval2  31876  dirkeritg  31884  dirkercncf  31889  fourierdlem29  31918  fourierdlem37  31926  fourierdlem62  31951  fourierdlem79  31968  fourierdlem81  31970  fourierdlem82  31971  fourierdlem92  31981  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem105  31994  fourierdlem108  31997  fourierdlem110  31999  fourierdlem112  32001  fourierdlem113  32002  fouriersw  32014  etransclem24  32041  etransclem25  32042  etransclem31  32048  etransclem35  32052  etransclem37  32054  mapdhval  37451  hdmap1fval  37524  hdmap1vallem  37525  hdmap1val  37526  hdmap1cbv  37530

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