Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifeqda Unicode version

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
StepHypRef Expression
1 iftrue 3947 . . . 4
21adantl 466 . . 3
3 ifeqda.1 . . 3
42, 3eqtrd 2498 . 2
5 iffalse 3950 . . . 4
65adantl 466 . . 3
7 ifeqda.2 . . 3
86, 7eqtrd 2498 . 2
94, 8pm2.61dan 791 1
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator