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

Theorem ifeq12d 3712
 Description: Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.)
Hypotheses
Ref Expression
ifeq1d.1
ifeq12d.2
Assertion
Ref Expression
ifeq12d

Proof of Theorem ifeq12d
StepHypRef Expression
1 ifeq1d.1 . . 3
21ifeq1d 3710 . 2
3 ifeq12d.2 . . 3
43ifeq2d 3711 . 2
52, 4eqtrd 2433 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1649  cif 3696 This theorem is referenced by:  ifbieq12d  3718  oev  6708  dfac12r  7973  xaddpnf1  10758  ruclem1  12771  eucalgval  13014  gsumpropd  14717  gsumress  14718  mulgfval  14832  mulgpropd  14864  frgpup3lem  15350  subrgmvr  16465  isobs  16888  pcoval  18975  pcorevlem  18990  itg2const  19571  ditgeq3  19676  efrlim  20747  lgsval  21023  rpvmasum2  21145  gxfval  21765  gxval  21766  gsumpropd2lem  24142  xrhval  24306  itg2addnclem  26118  uvcfval  27063  dgrsub2  27169  hdmap1fval  32220 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-rab 2672  df-v 2915  df-un 3282  df-if 3697
 Copyright terms: Public domain W3C validator