Theorem ifeqda 3974

Description: Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018.)

Hypotheses

Ref	Expression
ifeqda.1
ifeqda.2

Assertion

Ref	Expression
ifeqda

Proof of Theorem ifeqda

Step	Hyp	Ref	Expression
1		iftrue 3947	. . . 4
2	1	adantl 466	. . 3
3		ifeqda.1	. . 3
4	2, 3	eqtrd 2498	. 2
5		iffalse 3950	. . . 4
6	5	adantl 466	. . 3
7		ifeqda.2	. . 3
8	6, 7	eqtrd 2498	. 2
9	4, 8	pm2.61dan 791	1

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

This theorem is referenced by:  somincom  5409  cantnfp1  8121  ccatsymb  12600  swrdccat3blem  12720  repswccat  12757  ccatco  12801  bitsinvp1  14099  xrsdsreval  18463  fvmptnn04if  19350  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  oprpiece1res2  21452  phtpycc  21491  atantayl2  23269  ccatmulgnn0dir  28496  plymulx  28505  elmrsubrn  28880  fourierdlem101  31990  linc0scn0  33024

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-if 3942