Theorem ifbieq12d 3968

Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
ifbieq12d.1
ifbieq12d.2
ifbieq12d.3

Assertion

Ref	Expression
ifbieq12d

Proof of Theorem ifbieq12d

Step	Hyp	Ref	Expression
1		ifbieq12d.1	. . 3
2	1	ifbid 3963	. 2
3		ifbieq12d.2	. . 3
4		ifbieq12d.3	. . 3
5	3, 4	ifeq12d 3961	. 2
6	2, 5	eqtrd 2498	1

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

This theorem is referenced by:  csbif  3991  csbifgOLD  3992  tz7.44-2  7092  tz7.44-3  7093  boxcutc  7532  unxpdomlem1  7744  dfac12lem1  8544  dfac12r  8547  fin23lem12  8732  fin23lem33  8746  ttukeylem3  8912  ttukey2g  8917  xaddval  11451  seqf1olem2  12147  expval  12168  ccatfval  12592  ccatval1  12595  ccatval2  12596  ruclem1  13964  eucalgval2  14210  ressval  14684  gsumvalx  15897  gsumpropd  15899  gsumpropd2lem  15900  gsumress  15903  mulgval  16144  pmtrfv  16477  mvrfval  18076  xrsdsval  18462  marrepeval  19065  marepveval  19070  mdetunilem9  19122  madutpos  19144  madugsum  19145  minmar1eval  19151  symgmatr01lem  19155  symgmatr01  19156  gsummatr01lem3  19159  gsummatr01lem4  19160  gsummatr01  19161  ptcmplem3  20554  xrhmeo  21446  phtpycc  21491  pcovalg  21512  pcocn  21517  pcohtpylem  21519  pcoass  21524  pcorevlem  21526  ovolunlem1a  21907  ovolunlem1  21908  ioombl1  21972  mbfmax  22056  mbfpos  22058  mbfi1fseqlem2  22123  mbfi1fseq  22128  ditgeq1  22252  ditgeq2  22253  ig1pval  22573  cxpval  23045  musumsum  23468  muinv  23469  lgsval  23575  clwlkisclwwlklem2fv1  24782  gxval  25260  resvval  27817  ballotlemsv  28448  ballotlemsf1o  28452  plymulx0  28504  lgamgulmlem4  28574  lgamgulmlem5  28575  mrsubcv  28870  mrsubrn  28873  rdgprc0  29226  dfrdg2  29228  itg2addnclem3  30068  itgaddnclem2  30074  ftc1anclem5  30094  aomclem8  31007  ifeq123d  31432  icccncfext  31690  dvnxpaek  31739  cdleme27b  36094  cdleme29b  36101  cdleme31sn  36106  cdleme31fv  36116  cdleme40v  36195  dihffval  36957  dihfval  36958  dihval  36959

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