Theorem ifbieq2d 4061

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-un 3545  df-if 4037

This theorem is referenced by:  tz7.44-2  7390  tz7.44-3  7391  oev  7481  cantnfp1lem1  8458  cantnfp1lem3  8460  fin23lem12  9036  fin23lem33  9050  axcc2  9142  ttukeylem3  9216  ttukey2g  9221  canthp1lem2  9354  canthp1  9355  xnegeq  11912  xaddval  11928  xmulval  11930  expval  12724  cshfn  13387  ofccat  13556  relexpsucnnr  13613  sgnval  13676  sadcp1  15015  smupp1  15040  gcdval  15056  gcdass  15102  lcmval  15143  lcmass  15165  lcmfval  15172  lcmf0val  15173  lcmfpr  15178  iserodd  15378  pcval  15387  vdwlem6  15528  ramub1lem2  15569  ramcl  15571  mulgval  17366  symgextfv  17661  symgfixfo  17682  odval  17776  submod  17807  gexval  17816  znval  19702  fvmptnn04if  20473  cpmadumatpoly  20507  cayleyhamilton  20514  cayleyhamiltonALT  20515  ptcmplem2  21667  iccpnfhmeo  22552  pcopt  22630  ioombl1  23137  ioorval  23148  uniioombllem6  23162  itg1addlem3  23271  itg2uba  23316  limcfval  23442  limcmpt  23453  limcco  23463  dvcobr  23515  ig1pval  23736  abelthlem9  23998  logtayllem  24205  logtayl  24206  leibpilem2  24468  rlimcnp2  24493  efrlim  24496  igamval  24573  muval  24658  lgsval  24826  lgsfval  24827  lgsval2lem  24832  rpvmasum2  25001  padicval  25106  padicabv  25119  axlowdimlem15  25636  axlowdim  25641  eupath2lem3  26506  eupath2  26507  sgnsv  29058  sgnsval  29059  psgnfzto1stlem  29181  madjusmdetlem2  29222  madjusmdet  29225  xrge0iifcv  29308  xrge0iifhom  29311  xrge0tmdOLD  29319  xrge0tmd  29320  signspval  29955  rdgprc0  30943  dfrdg2  30945  dfrdg4  31228  csbrdgg  32351  finxpeq1  32399  finxpreclem3  32406  poimirlem1  32580  poimirlem7  32586  poimirlem10  32589  poimirlem11  32590  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  fdc  32711  heiborlem4  32783  heiborlem6  32785  heiborlem10  32789  mapdhval  36031  hdmap1fval  36104  hdmap1vallem  36105  hdmap1val  36106  hdmap1cbv  36110  irrapxlem4  36407  clsk1indlem0  37359  clsk1indlem2  37360  clsk1indlem3  37361  clsk1indlem4  37362  clsk1indlem1  37363  dirkerval2  38987  dirkeritg  38995  dirkercncf  39000  fourierdlem29  39029  fourierdlem37  39037  fourierdlem62  39061  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem92  39091  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem105  39104  fourierdlem108  39107  fourierdlem110  39109  fourierdlem112  39111  fourierdlem113  39112  fouriersw  39124  etransclem24  39151  etransclem25  39152  etransclem31  39158  etransclem35  39162  etransclem37  39164  sge0val  39259  nnfoctbdjlem  39348  nnfoctbdj  39349  ovnval  39431  ovnval2  39435  ovnval2b  39442  hsphoif  39466  hoidmvval  39467  hsphoival  39469  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmv1le  39484  ovnhoi  39493  hoidifhspval  39498  hspmbllem2  39517  ovnsubadd2  39536  eupth2lem3lem3  41398  eupth2  41407  eucrct2eupth  41413  blenval  42163