Theorem ifeq12d 4548

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 4546	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		ifeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	ifeq2d 4547	. 2 ⊢ (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷))
5	2, 4	eqtrd 2772	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

Syntax hints:   → wi 4   = wceq 1541  ifcif 4527

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-un 3952  df-if 4528

This theorem is referenced by:  ifbieq12d  4555  csbif  4584  oev  8510  dfac12r  10137  xaddpnf1  13201  swrdccat3blem  14685  relexpsucnnr  14968  ruclem1  16170  eucalgval  16515  gsumpropd  18593  gsumpropd2lem  18594  gsumress  18597  mulgfval  18946  mulgfvalALT  18947  mulgpropd  18990  frgpup3lem  19639  isobs  21266  uvcfval  21330  subrgmvr  21579  matsc  21943  scmatscmide  22000  marrepval0  22054  marepvval0  22059  mulmarep1el  22065  madufval  22130  madugsum  22136  minmar1fval  22139  pmat1opsc  22192  pmat1ovscd  22193  mat2pmat1  22225  decpmatid  22263  idpm2idmp  22294  pcoval  24518  pcorevlem  24533  itg2const  25249  ditgeq3  25358  efrlim  26463  lgsval  26793  rpvmasum2  27004  fzto1st  32249  psgnfzto1st  32251  xrhval  32986  itg2addnclem  36527  ftc1anclem5  36553  hdmap1fval  40655  sticksstones12a  40961  sticksstones12  40962  rhmmpl  41122  selvvvval  41154  fsuppind  41159  dgrsub2  41862  reabssgn  42372  dirkerval  44793  fourierdlem111  44919  fourierdlem112  44920  fourierdlem113  44921  hsphoif  45278  hsphoival  45281  hoidmvlelem5  45301  hoidifhspval2  45317  hspmbllem2  45329  itcoval  47300