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

Theorem ifeq12d 4248
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 4246 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 ifeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43ifeq2d 4247 . 2 (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷))
52, 4eqtrd 2792 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  ifcif 4228
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-rab 3057  df-v 3340  df-un 3718  df-if 4229
This theorem is referenced by:  ifbieq12d  4255  csbif  4280  oev  7761  dfac12r  9158  xaddpnf1  12248  swrdccat3blem  13693  relexpsucnnr  13962  ruclem1  15157  eucalgval  15495  gsumpropd  17471  gsumpropd2lem  17472  gsumress  17475  mulgfval  17741  mulgpropd  17783  frgpup3lem  18388  subrgmvr  19661  isobs  20264  uvcfval  20323  matsc  20456  scmatscmide  20513  marrepval0  20567  marepvval0  20572  mulmarep1el  20578  madufval  20643  madugsum  20649  minmar1fval  20652  pmat1opsc  20704  pmat1ovscd  20705  mat2pmat1  20737  decpmatid  20775  idpm2idmp  20806  pcoval  23009  pcorevlem  23024  itg2const  23704  ditgeq3  23811  efrlim  24893  lgsval  25223  rpvmasum2  25398  fzto1st  30160  psgnfzto1st  30162  xrhval  30369  itg2addnclem  33772  ftc1anclem5  33800  hdmap1fval  37586  dgrsub2  38205  dirkerval  40809  fourierdlem111  40935  fourierdlem112  40936  fourierdlem113  40937  hsphoif  41294  hsphoival  41297  hoidmvlelem5  41317  hoidifhspval2  41333  hspmbllem2  41345
  Copyright terms: Public domain W3C validator