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

Theorem ifeq12d 4460
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 4458 . 2 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3 ifeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43ifeq2d 4459 . 2 (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷))
52, 4eqtrd 2856 1 (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  ifcif 4440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-rab 3135  df-v 3473  df-un 3915  df-if 4441
This theorem is referenced by:  ifbieq12d  4467  csbif  4495  oev  8114  dfac12r  9549  xaddpnf1  12597  swrdccat3blem  14080  relexpsucnnr  14363  ruclem1  15563  eucalgval  15903  gsumpropd  17866  gsumpropd2lem  17867  gsumress  17870  mulgfval  18204  mulgfvalALT  18205  mulgpropd  18247  frgpup3lem  18881  subrgmvr  20217  isobs  20839  uvcfval  20903  matsc  21034  scmatscmide  21091  marrepval0  21145  marepvval0  21150  mulmarep1el  21156  madufval  21221  madugsum  21227  minmar1fval  21230  pmat1opsc  21282  pmat1ovscd  21283  mat2pmat1  21315  decpmatid  21353  idpm2idmp  21384  pcoval  23594  pcorevlem  23609  itg2const  24322  ditgeq3  24431  efrlim  25533  lgsval  25863  rpvmasum2  26074  fzto1st  30752  psgnfzto1st  30754  xrhval  31266  itg2addnclem  34988  ftc1anclem5  35014  hdmap1fval  38972  dgrsub2  39876  dirkerval  42526  fourierdlem111  42652  fourierdlem112  42653  fourierdlem113  42654  hsphoif  43008  hsphoival  43011  hoidmvlelem5  43031  hoidifhspval2  43047  hspmbllem2  43059  itcoval  44837
  Copyright terms: Public domain W3C validator