Theorem ifbieq2d 4574

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-if 4549

This theorem is referenced by:  tz7.44-2  8463  tz7.44-3  8464  oev  8570  cantnfp1lem1  9747  cantnfp1lem3  9749  ttrclselem2  9795  fin23lem12  10400  fin23lem33  10414  axcc2  10506  ttukeylem3  10580  ttukey2g  10585  canthp1lem2  10722  canthp1  10723  xnegeq  13269  xaddval  13285  xmulval  13287  expval  14114  cshfn  14838  ofccat  15018  relexpsucnnr  15074  sgnval  15137  sadcp1  16501  smupp1  16526  gcdval  16542  gcdass  16594  lcmval  16639  lcmass  16661  lcmfval  16668  lcmf0val  16669  lcmfpr  16674  iserodd  16882  pcval  16891  vdwlem6  17033  ramub1lem2  17074  ramcl  17076  mulgval  19111  symgextfv  19460  symgfixfo  19481  odfval  19574  odval  19576  submod  19611  gexval  19620  znval  21573  fvmptnn04if  22876  cpmadumatpoly  22910  cayleyhamilton  22917  cayleyhamiltonALT  22918  ptcmplem2  24082  iccpnfhmeo  24995  pcopt  25074  ioombl1  25616  ioorval  25628  uniioombllem6  25642  itg1addlem3  25752  itg2uba  25798  limcfval  25927  limcmpt  25938  limcco  25948  dvcobr  26003  dvcobrOLD  26004  ig1pval  26235  abelthlem9  26502  logtayllem  26719  logtayl  26720  leibpilem2  27002  rlimcnp2  27027  efrlim  27030  efrlimOLD  27031  igamval  27108  muval  27193  lgsval  27363  lgsfval  27364  lgsval2lem  27369  rpvmasum2  27574  padicval  27679  padicabv  27692  expsval  28426  axlowdimlem15  28989  axlowdim  28994  eupth2lem3lem3  30262  eupth2  30271  eucrct2eupth  30277  psgnfzto1stlem  33093  sgnsv  33153  sgnsval  33154  madjusmdetlem2  33774  madjusmdet  33777  xrge0iifcv  33880  xrge0iifhom  33883  xrge0tmd  33891  xrge0tmdALT  33892  signspval  34529  ex-sategoelel  35389  rdgprc0  35757  dfrdg2  35759  dfrdg4  35915  csbrdgg  37295  finxpeq1  37352  finxpreclem3  37359  poimirlem1  37581  poimirlem7  37587  poimirlem10  37590  poimirlem11  37591  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  fdc  37705  heiborlem4  37774  heiborlem6  37776  heiborlem10  37780  mapdhval  41681  hdmap1fval  41753  hdmap1vallem  41754  hdmap1val  41755  hdmap1cbv  41759  sticksstones10  42112  sticksstones12a  42114  metakunt3  42164  metakunt4  42165  metakunt6  42167  metakunt7  42168  metakunt8  42169  metakunt10  42171  metakunt11  42172  metakunt12  42173  metakunt20  42181  metakunt21  42182  metakunt22  42183  fsuppind  42545  irrapxlem4  42781  clsk1indlem0  44003  clsk1indlem2  44004  clsk1indlem3  44005  clsk1indlem4  44006  clsk1indlem1  44007  dirkerval2  46015  dirkeritg  46023  dirkercncf  46028  fourierdlem29  46057  fourierdlem37  46065  fourierdlem62  46089  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem92  46119  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem105  46132  fourierdlem108  46135  fourierdlem110  46137  fourierdlem112  46139  fourierdlem113  46140  fouriersw  46152  etransclem24  46179  etransclem25  46180  etransclem31  46186  etransclem35  46190  etransclem37  46192  sge0val  46287  nnfoctbdjlem  46376  nnfoctbdj  46377  ovnval  46462  ovnval2  46466  ovnval2b  46473  hsphoif  46497  hoidmvval  46498  hsphoival  46500  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmv1le  46515  ovnhoi  46524  hoidifhspval  46529  hspmbllem2  46548  ovnsubadd2  46567  blenval  48305