Theorem ifeq1d 3959

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

Hypothesis

Ref	Expression
ifeq1d.1

Assertion

Ref	Expression
ifeq1d

Proof of Theorem ifeq1d

Step	Hyp	Ref	Expression
1		ifeq1d.1	. 2
2		ifeq1 3945	. 2
3	1, 2	syl 16	1

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

This theorem is referenced by:  ifeq12d  3961  ifbieq1d  3964  ifeq1da  3971  rabsnif  4099  fsuppmptif  7879  cantnflem1  8129  cantnflem1dOLD  8151  cantnflem1OLD  8152  sumeq2w  13514  cbvsum  13517  isumless  13657  prodss  13754  subgmulg  16215  gsumzsplitOLD  16945  evlslem2  18180  dmatcrng  19004  scmatscmiddistr  19010  scmatcrng  19023  marrepfval  19062  mdetr0  19107  mdetunilem8  19121  madufval  19139  madugsum  19145  minmar1fval  19148  decpmatid  19271  monmatcollpw  19280  pmatcollpwscmatlem1  19290  cnmpt2pc  21428  pcoval2  21516  pcopt  21522  itgz  22187  iblss2  22212  itgss  22218  itgcn  22249  plyeq0lem  22607  dgrcolem2  22671  plydivlem4  22692  leibpi  23273  chtublem  23486  sumdchr  23547  bposlem6  23564  lgsval  23575  dchrvmasumiflem2  23687  padicabvcxp  23817  dfrdg3  29229  ftc1anclem2  30091  ftc1anclem5  30094  ftc1anclem7  30096

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