Theorem ifeq12d 4498

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-un 3903  df-if 4477

This theorem is referenced by:  ifbieq12d  4505  csbif  4534  oev  8437  dfac12r  10047  xaddpnf1  13129  swrdccat3blem  14650  relexpsucnnr  14936  ruclem1  16144  eucalgval  16497  gsumpropd  18590  gsumpropd2lem  18591  gsumress  18594  mulgfval  18986  mulgfvalALT  18987  mulgpropd  19033  frgpup3lem  19693  isobs  21661  uvcfval  21725  psrascl  21919  subrgmvr  21971  psdmvr  22087  rhmmpl  22301  rhmply1vr1  22305  matsc  22368  scmatscmide  22425  marrepval0  22479  marepvval0  22484  mulmarep1el  22490  madufval  22555  madugsum  22561  minmar1fval  22564  pmat1opsc  22617  pmat1ovscd  22618  mat2pmat1  22650  decpmatid  22688  idpm2idmp  22719  pcoval  24941  pcorevlem  24956  itg2const  25671  ditgeq3  25781  efrlim  26909  efrlimOLD  26910  lgsval  27242  rpvmasum2  27453  expsval  28351  fzto1st  33081  psgnfzto1st  33083  extvval  33584  xrhval  34054  cbvditgdavw  36349  itg2addnclem  37734  ftc1anclem5  37760  hdmap1fval  41918  sticksstones12a  42273  sticksstones12  42274  rhmpsr  42673  selvvvval  42706  fsuppind  42711  dgrsub2  43255  reabssgn  43756  dirkerval  46216  fourierdlem111  46342  fourierdlem112  46343  fourierdlem113  46344  hsphoif  46701  hsphoival  46704  hoidmvlelem5  46724  hoidifhspval2  46740  hspmbllem2  46752  itcoval  48789