Theorem ifeq2d 3960

Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)

Hypothesis

Ref	Expression
ifeq1d.1

Assertion

Ref	Expression
ifeq2d

Proof of Theorem ifeq2d

Step	Hyp	Ref	Expression
1		ifeq1d.1	. 2
2		ifeq2 3946	. 2
3	1, 2	syl 16	1

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

This theorem is referenced by:  ifeq12d  3961  ifbieq2d  3966  ifeq2da  3972  ifcomnan  3990  rdgeq1  7096  cantnflem1d  8128  cantnflem1  8129  cantnflem1dOLD  8151  cantnflem1OLD  8152  rexmul  11492  1arithlem4  14444  ramcl  14547  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  subrgascl  18163  scmatscm  19015  marrepfval  19062  ma1repveval  19073  mulmarep1el  19074  mdetralt2  19111  mdetunilem8  19121  maduval  19140  maducoeval2  19142  madurid  19146  minmar1val0  19149  monmatcollpw  19280  pmatcollpwscmatlem1  19290  monmat2matmon  19325  itg2monolem1  22157  iblmulc2  22237  itgmulc2lem1  22238  bddmulibl  22245  dvtaylp  22765  dchrinvcl  23528  rpvmasum2  23697  padicfval  23801  gxval  25260  plymulx  28505  itg2addnclem  30066  itg2addnclem3  30068  itg2addnc  30069  itgmulc2nclem1  30081  itgioocnicc  31776  etransclem14  32031  etransclem17  32034  etransclem21  32038  etransclem25  32042  etransclem28  32045  etransclem31  32048  hdmap1fval  37524

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