Theorem ifeq12d 4106

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

Syntax hints:   → wi 4   = wceq 1483  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-un 3579  df-if 4087

This theorem is referenced by:  ifbieq12d  4113  csbif  4138  oev  7594  dfac12r  8968  xaddpnf1  12057  swrdccat3blem  13495  relexpsucnnr  13765  ruclem1  14960  eucalgval  15295  gsumpropd  17272  gsumpropd2lem  17273  gsumress  17276  mulgfval  17542  mulgpropd  17584  frgpup3lem  18190  subrgmvr  19461  isobs  20064  uvcfval  20123  matsc  20256  scmatscmide  20313  marrepval0  20367  marepvval0  20372  mulmarep1el  20378  madufval  20443  madugsum  20449  minmar1fval  20452  pmat1opsc  20504  pmat1ovscd  20505  mat2pmat1  20537  decpmatid  20575  idpm2idmp  20606  pcoval  22811  pcorevlem  22826  itg2const  23507  ditgeq3  23614  efrlim  24696  lgsval  25026  rpvmasum2  25201  fzto1st  29853  psgnfzto1st  29855  xrhval  30062  itg2addnclem  33461  ftc1anclem5  33489  hdmap1fval  37086  dgrsub2  37705  dirkerval  40308  fourierdlem111  40434  fourierdlem112  40435  fourierdlem113  40436  hsphoif  40790  hsphoival  40793  hoidmvlelem5  40813  hoidifhspval2  40829  hspmbllem2  40841