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

Theorem ifeq12d 4508
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 4506 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 ifeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43ifeq2d 4507 . 2 (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷))
52, 4eqtrd 2777 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  ifcif 4487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409  df-v 3448  df-un 3916  df-if 4488
This theorem is referenced by:  ifbieq12d  4515  csbif  4544  oev  8461  dfac12r  10083  xaddpnf1  13146  swrdccat3blem  14628  relexpsucnnr  14911  ruclem1  16114  eucalgval  16459  gsumpropd  18534  gsumpropd2lem  18535  gsumress  18538  mulgfval  18875  mulgfvalALT  18876  mulgpropd  18919  frgpup3lem  19560  isobs  21129  uvcfval  21193  subrgmvr  21437  matsc  21802  scmatscmide  21859  marrepval0  21913  marepvval0  21918  mulmarep1el  21924  madufval  21989  madugsum  21995  minmar1fval  21998  pmat1opsc  22051  pmat1ovscd  22052  mat2pmat1  22084  decpmatid  22122  idpm2idmp  22153  pcoval  24377  pcorevlem  24392  itg2const  25108  ditgeq3  25217  efrlim  26322  lgsval  26652  rpvmasum2  26863  fzto1st  31955  psgnfzto1st  31957  xrhval  32602  itg2addnclem  36132  ftc1anclem5  36158  hdmap1fval  40262  sticksstones12a  40568  sticksstones12  40569  rhmmpl  40744  fsuppind  40768  mhphf  40774  dgrsub2  41465  reabssgn  41915  dirkerval  44339  fourierdlem111  44465  fourierdlem112  44466  fourierdlem113  44467  hsphoif  44824  hsphoival  44827  hoidmvlelem5  44847  hoidifhspval2  44863  hspmbllem2  44875  itcoval  46754
  Copyright terms: Public domain W3C validator