Theorem ifeq12d 4327

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

Step	Hyp	Ref	Expression
1		ifeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	ifeq1d 4325	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		ifeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	ifeq2d 4326	. 2 ⊢ (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷))
5	2, 4	eqtrd 2814	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

Syntax hints:   → wi 4   = wceq 1601  ifcif 4307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-un 3797  df-if 4308

This theorem is referenced by:  ifbieq12d  4334  csbif  4362  oev  7878  dfac12r  9303  xaddpnf1  12369  swrdccat3blem  13871  relexpsucnnr  14172  ruclem1  15364  eucalgval  15701  gsumpropd  17658  gsumpropd2lem  17659  gsumress  17662  mulgfval  17929  mulgpropd  17968  frgpup3lem  18576  subrgmvr  19858  isobs  20463  uvcfval  20527  matsc  20661  scmatscmide  20718  marrepval0  20772  marepvval0  20777  mulmarep1el  20783  madufval  20848  madugsum  20854  minmar1fval  20857  pmat1opsc  20911  pmat1ovscd  20912  mat2pmat1  20944  decpmatid  20982  idpm2idmp  21013  pcoval  23218  pcorevlem  23233  itg2const  23944  ditgeq3  24051  efrlim  25148  lgsval  25478  rpvmasum2  25653  fzto1st  30451  psgnfzto1st  30453  xrhval  30660  itg2addnclem  34088  ftc1anclem5  34116  hdmap1fval  37952  dgrsub2  38668  dirkerval  41239  fourierdlem111  41365  fourierdlem112  41366  fourierdlem113  41367  hsphoif  41721  hsphoival  41724  hoidmvlelem5  41744  hoidifhspval2  41760  hspmbllem2  41772