Theorem ifeq1da 3971

Description: Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypothesis

Ref	Expression
ifeq1da.1

Assertion

Ref	Expression
ifeq1da

Proof of Theorem ifeq1da

Step	Hyp	Ref	Expression
1		ifeq1da.1	. . 3
2	1	ifeq1d 3959	. 2
3		iffalse 3950	. . . 4
4		iffalse 3950	. . . 4
5	3, 4	eqtr4d 2501	. . 3
6	5	adantl 466	. 2
7	2, 6	pm2.61dan 791	1

Syntax hints:  -.wn 3  ->wi 4  /\wa 369  =wceq 1395  ifcif 3941

This theorem is referenced by:  cantnflem1d  8128  cantnflem1  8129  cantnflem1dOLD  8151  cantnflem1OLD  8152  dfac12lem1  8544  xrmaxeq  11409  xrmineq  11410  rexmul  11492  max0add  13143  sumeq2ii  13515  fsumser  13552  ramcl  14547  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  coe1pwmul  18320  scmatscmiddistr  19010  mulmarep1gsum1  19075  maducoeval2  19142  madugsum  19145  madurid  19146  ptcld  20114  copco  21518  ibllem  22171  itgvallem3  22192  iblposlem  22198  iblss2  22212  iblmulc2  22237  cnplimc  22291  limcco  22297  dvexp3  22379  dchrinvcl  23528  lgsval2lem  23581  lgsval4lem  23582  lgsneg  23594  lgsmod  23596  lgsdilem2  23606  rpvmasum2  23697  mrsubrn  28873  ftc1anclem6  30095  ftc1anclem8  30097

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