Theorem ifeq2da 3972

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

Hypothesis

Ref	Expression
ifeq2da.1

Assertion

Ref	Expression
ifeq2da

Proof of Theorem ifeq2da

Step	Hyp	Ref	Expression
1		iftrue 3947	. . . 4
2		iftrue 3947	. . . 4
3	1, 2	eqtr4d 2501	. . 3
4	3	adantl 466	. 2
5		ifeq2da.1	. . 3
6	5	ifeq2d 3960	. 2
7	4, 6	pm2.61dan 791	1

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

This theorem is referenced by:  dfac12lem1  8544  ttukeylem3  8912  xmulcom  11487  xmulneg1  11490  subgmulg  16215  1marepvmarrepid  19077  copco  21518  pcopt2  21523  limcdif  22280  limcmpt  22287  limcres  22290  limccnp  22295  radcnv0  22811  leibpi  23273  efrlim  23299  dchrvmasumiflem2  23687  rpvmasum2  23697  padicabvf  23816  padicabvcxp  23817  itg2addnclem  30066  fourierdlem73  31962  fourierdlem76  31965  fourierdlem89  31978  fourierdlem91  31980

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