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 2770	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

Syntax hints:   → wi 4   = wceq 1539  ifcif 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-un 3952  df-if 4528

This theorem is referenced by:  ifbieq12d  4555  csbif  4584  oev  8516  dfac12r  10143  xaddpnf1  13209  swrdccat3blem  14693  relexpsucnnr  14976  ruclem1  16178  eucalgval  16523  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  mulgfval  18988  mulgfvalALT  18989  mulgpropd  19032  frgpup3lem  19686  isobs  21494  uvcfval  21558  subrgmvr  21807  matsc  22172  scmatscmide  22229  marrepval0  22283  marepvval0  22288  mulmarep1el  22294  madufval  22359  madugsum  22365  minmar1fval  22368  pmat1opsc  22421  pmat1ovscd  22422  mat2pmat1  22454  decpmatid  22492  idpm2idmp  22523  pcoval  24758  pcorevlem  24773  itg2const  25490  ditgeq3  25599  efrlim  26710  lgsval  27040  rpvmasum2  27251  fzto1st  32532  psgnfzto1st  32534  xrhval  33296  itg2addnclem  36842  ftc1anclem5  36868  hdmap1fval  40970  sticksstones12a  41279  sticksstones12  41280  rhmmpl  41427  selvvvval  41459  fsuppind  41464  dgrsub2  42179  reabssgn  42689  dirkerval  45105  fourierdlem111  45231  fourierdlem112  45232  fourierdlem113  45233  hsphoif  45590  hsphoival  45593  hoidmvlelem5  45613  hoidifhspval2  45629  hspmbllem2  45641  itcoval  47434