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

Theorem ifeq12d 4139
Description: Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.)
Hypotheses
Ref Expression
ifeq1d.1 (𝜑𝐴 = 𝐵)
ifeq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
ifeq12d (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

Proof of Theorem ifeq12d
StepHypRef Expression
1 ifeq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21ifeq1d 4137 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 ifeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43ifeq2d 4138 . 2 (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷))
52, 4eqtrd 2685 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-un 3612  df-if 4120
This theorem is referenced by:  ifbieq12d  4146  csbif  4171  oev  7639  dfac12r  9006  xaddpnf1  12095  swrdccat3blem  13541  relexpsucnnr  13809  ruclem1  15004  eucalgval  15342  gsumpropd  17319  gsumpropd2lem  17320  gsumress  17323  mulgfval  17589  mulgpropd  17631  frgpup3lem  18236  subrgmvr  19509  isobs  20112  uvcfval  20171  matsc  20304  scmatscmide  20361  marrepval0  20415  marepvval0  20420  mulmarep1el  20426  madufval  20491  madugsum  20497  minmar1fval  20500  pmat1opsc  20552  pmat1ovscd  20553  mat2pmat1  20585  decpmatid  20623  idpm2idmp  20654  pcoval  22857  pcorevlem  22872  itg2const  23552  ditgeq3  23659  efrlim  24741  lgsval  25071  rpvmasum2  25246  fzto1st  29981  psgnfzto1st  29983  xrhval  30190  itg2addnclem  33591  ftc1anclem5  33619  hdmap1fval  37403  dgrsub2  38022  dirkerval  40626  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  hsphoif  41111  hsphoival  41114  hoidmvlelem5  41134  hoidifhspval2  41150  hspmbllem2  41162
  Copyright terms: Public domain W3C validator