Theorem ifbieq2d 4556

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 4553	. 2 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐴))
3		ifbieq2d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq2d 4550	. 2 ⊢ (𝜑 → if(𝜒, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))
5	2, 4	eqtrd 2774	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-un 3967  df-if 4531

This theorem is referenced by:  tz7.44-2  8445  tz7.44-3  8446  oev  8550  cantnfp1lem1  9715  cantnfp1lem3  9717  ttrclselem2  9763  fin23lem12  10368  fin23lem33  10382  axcc2  10474  ttukeylem3  10548  ttukey2g  10553  canthp1lem2  10690  canthp1  10691  xnegeq  13245  xaddval  13261  xmulval  13263  expval  14100  cshfn  14824  ofccat  15004  relexpsucnnr  15060  sgnval  15123  sadcp1  16488  smupp1  16513  gcdval  16529  gcdass  16580  lcmval  16625  lcmass  16647  lcmfval  16654  lcmf0val  16655  lcmfpr  16660  iserodd  16868  pcval  16877  vdwlem6  17019  ramub1lem2  17060  ramcl  17062  mulgval  19101  symgextfv  19450  symgfixfo  19471  odfval  19564  odval  19566  submod  19601  gexval  19610  znval  21567  fvmptnn04if  22870  cpmadumatpoly  22904  cayleyhamilton  22911  cayleyhamiltonALT  22912  ptcmplem2  24076  iccpnfhmeo  24989  pcopt  25068  ioombl1  25610  ioorval  25622  uniioombllem6  25636  itg1addlem3  25746  itg2uba  25792  limcfval  25921  limcmpt  25932  limcco  25942  dvcobr  25997  dvcobrOLD  25998  ig1pval  26229  abelthlem9  26498  logtayllem  26715  logtayl  26716  leibpilem2  26998  rlimcnp2  27023  efrlim  27026  efrlimOLD  27027  igamval  27104  muval  27189  lgsval  27359  lgsfval  27360  lgsval2lem  27365  rpvmasum2  27570  padicval  27675  padicabv  27688  expsval  28422  axlowdimlem15  28985  axlowdim  28990  eupth2lem3lem3  30258  eupth2  30267  eucrct2eupth  30273  psgnfzto1stlem  33102  sgnsv  33162  sgnsval  33163  madjusmdetlem2  33788  madjusmdet  33791  xrge0iifcv  33894  xrge0iifhom  33897  xrge0tmd  33905  xrge0tmdALT  33906  signspval  34545  ex-sategoelel  35405  rdgprc0  35774  dfrdg2  35776  dfrdg4  35932  csbrdgg  37311  finxpeq1  37368  finxpreclem3  37375  poimirlem1  37607  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  itg2addnclem  37657  itg2addnclem3  37659  itg2addnc  37660  fdc  37731  heiborlem4  37800  heiborlem6  37802  heiborlem10  37806  mapdhval  41706  hdmap1fval  41778  hdmap1vallem  41779  hdmap1val  41780  hdmap1cbv  41784  sticksstones10  42136  sticksstones12a  42138  metakunt3  42188  metakunt4  42189  metakunt6  42191  metakunt7  42192  metakunt8  42193  metakunt10  42195  metakunt11  42196  metakunt12  42197  metakunt20  42205  metakunt21  42206  metakunt22  42207  fsuppind  42576  irrapxlem4  42812  clsk1indlem0  44030  clsk1indlem2  44031  clsk1indlem3  44032  clsk1indlem4  44033  clsk1indlem1  44034  dirkerval2  46049  dirkeritg  46057  dirkercncf  46062  fourierdlem29  46091  fourierdlem37  46099  fourierdlem62  46123  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem92  46153  fourierdlem96  46157  fourierdlem97  46158  fourierdlem98  46159  fourierdlem99  46160  fourierdlem105  46166  fourierdlem108  46169  fourierdlem110  46171  fourierdlem112  46173  fourierdlem113  46174  fouriersw  46186  etransclem24  46213  etransclem25  46214  etransclem31  46220  etransclem35  46224  etransclem37  46226  sge0val  46321  nnfoctbdjlem  46410  nnfoctbdj  46411  ovnval  46496  ovnval2  46500  ovnval2b  46507  hsphoif  46531  hoidmvval  46532  hsphoival  46534  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmv1le  46549  ovnhoi  46558  hoidifhspval  46563  hspmbllem2  46582  ovnsubadd2  46601  blenval  48420