Theorem ifbieq2d 4527

Description: Equivalence/equality deduction for conditional operators. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypotheses

Ref	Expression
ifbieq2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq2d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifbieq2d	⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

Proof of Theorem ifbieq2d

Step	Hyp	Ref	Expression
1		ifbieq2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 4524	. 2 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3		ifbieq2d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq2d 4521	. 2 ⊢ (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
5	2, 4	eqtrd 2770	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4500

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-un 3931  df-if 4501

This theorem is referenced by:  tz7.44-2  8419  tz7.44-3  8420  oev  8524  cantnfp1lem1  9690  cantnfp1lem3  9692  ttrclselem2  9738  fin23lem12  10343  fin23lem33  10357  axcc2  10449  ttukeylem3  10523  ttukey2g  10528  canthp1lem2  10665  canthp1  10666  xnegeq  13221  xaddval  13237  xmulval  13239  expval  14079  cshfn  14806  ofccat  14986  relexpsucnnr  15042  sgnval  15105  sadcp1  16472  smupp1  16497  gcdval  16513  gcdass  16564  lcmval  16609  lcmass  16631  lcmfval  16638  lcmf0val  16639  lcmfpr  16644  iserodd  16853  pcval  16862  vdwlem6  17004  ramub1lem2  17045  ramcl  17047  mulgval  19052  symgextfv  19397  symgfixfo  19418  odfval  19511  odval  19513  submod  19548  gexval  19557  znval  21494  fvmptnn04if  22785  cpmadumatpoly  22819  cayleyhamilton  22826  cayleyhamiltonALT  22827  ptcmplem2  23989  iccpnfhmeo  24892  pcopt  24971  ioombl1  25513  ioorval  25525  uniioombllem6  25539  itg1addlem3  25649  itg2uba  25694  limcfval  25823  limcmpt  25834  limcco  25844  dvcobr  25899  dvcobrOLD  25900  ig1pval  26131  abelthlem9  26400  logtayllem  26618  logtayl  26619  leibpilem2  26901  rlimcnp2  26926  efrlim  26929  efrlimOLD  26930  igamval  27007  muval  27092  lgsval  27262  lgsfval  27263  lgsval2lem  27268  rpvmasum2  27473  padicval  27578  padicabv  27591  expsval  28325  axlowdimlem15  28881  axlowdim  28886  eupth2lem3lem3  30157  eupth2  30166  eucrct2eupth  30172  psgnfzto1stlem  33057  sgnsv  33117  sgnsval  33118  madjusmdetlem2  33805  madjusmdet  33808  xrge0iifcv  33911  xrge0iifhom  33914  xrge0tmd  33922  xrge0tmdALT  33923  signspval  34530  ex-sategoelel  35389  rdgprc0  35757  dfrdg2  35759  dfrdg4  35915  csbrdgg  37293  finxpeq1  37350  finxpreclem3  37357  poimirlem1  37591  poimirlem7  37597  poimirlem10  37600  poimirlem11  37601  itg2addnclem  37641  itg2addnclem3  37643  itg2addnc  37644  fdc  37715  heiborlem4  37784  heiborlem6  37786  heiborlem10  37790  mapdhval  41689  hdmap1fval  41761  hdmap1vallem  41762  hdmap1val  41763  hdmap1cbv  41767  sticksstones10  42114  sticksstones12a  42116  metakunt3  42166  metakunt4  42167  metakunt6  42169  metakunt7  42170  metakunt8  42171  metakunt10  42173  metakunt11  42174  metakunt12  42175  metakunt20  42183  metakunt21  42184  metakunt22  42185  fsuppind  42560  irrapxlem4  42795  clsk1indlem0  44012  clsk1indlem2  44013  clsk1indlem3  44014  clsk1indlem4  44015  clsk1indlem1  44016  dirkerval2  46071  dirkeritg  46079  dirkercncf  46084  fourierdlem29  46113  fourierdlem37  46121  fourierdlem62  46145  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem92  46175  fourierdlem96  46179  fourierdlem97  46180  fourierdlem98  46181  fourierdlem99  46182  fourierdlem105  46188  fourierdlem108  46191  fourierdlem110  46193  fourierdlem112  46195  fourierdlem113  46196  fouriersw  46208  etransclem24  46235  etransclem25  46236  etransclem31  46242  etransclem35  46246  etransclem37  46248  sge0val  46343  nnfoctbdjlem  46432  nnfoctbdj  46433  ovnval  46518  ovnval2  46522  ovnval2b  46529  hsphoif  46553  hoidmvval  46554  hsphoival  46556  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmv1le  46571  ovnhoi  46580  hoidifhspval  46585  hspmbllem2  46604  ovnsubadd2  46623  blenval  48499