Theorem ifbieq2d 4504

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-un 3907  df-if 4478

This theorem is referenced by:  tz7.44-2  8371  tz7.44-3  8372  oev  8476  cantnfp1lem1  9626  cantnfp1lem3  9628  ttrclselem2  9674  fin23lem12  10281  fin23lem33  10295  axcc2  10387  ttukeylem3  10461  ttukey2g  10466  canthp1lem2  10604  canthp1  10605  xnegeq  13203  xaddval  13219  xmulval  13221  expval  14069  cshfn  14796  ofccat  14975  relexpsucnnr  15031  sgnval  15094  sadcp1  16479  smupp1  16504  gcdval  16520  gcdass  16571  lcmval  16616  lcmass  16638  lcmfval  16645  lcmf0val  16646  lcmfpr  16651  iserodd  16861  pcval  16870  vdwlem6  17012  ramub1lem2  17053  ramcl  17055  mulgval  19103  symgextfv  19448  symgfixfo  19469  odfval  19562  odval  19564  submod  19599  gexval  19608  znval  21574  fvmptnn04if  22896  cpmadumatpoly  22930  cayleyhamilton  22937  cayleyhamiltonALT  22938  ptcmplem2  24100  iccpnfhmeo  24994  pcopt  25071  ioombl1  25611  ioorval  25623  uniioombllem6  25637  itg1addlem3  25747  itg2uba  25792  limcfval  25921  limcmpt  25932  limcco  25942  dvcobr  25995  ig1pval  26223  abelthlem9  26490  logtayllem  26711  logtayl  26712  leibpilem2  26993  rlimcnp2  27018  efrlim  27021  igamval  27098  muval  27183  lgsval  27352  lgsfval  27353  lgsval2lem  27358  rpvmasum2  27563  padicval  27668  padicabv  27681  expsval  28505  axlowdimlem15  29113  axlowdim  29118  eupth2lem3lem3  30388  eupth2  30397  eucrct2eupth  30403  psgnfzto1stlem  33240  sgnsv  33300  sgnsval  33301  madjusmdetlem2  34085  madjusmdet  34088  xrge0iifcv  34191  xrge0iifhom  34194  xrge0tmd  34202  xrge0tmdALT  34203  signspval  34806  ex-sategoelel  35731  rdgprc0  36101  dfrdg2  36103  dfrdg4  36261  csbrdgg  37783  finxpeq1  37840  finxpreclem3  37847  poimirlem1  38080  poimirlem7  38086  poimirlem10  38089  poimirlem11  38090  itg2addnclem  38130  itg2addnclem3  38132  itg2addnc  38133  fdc  38204  heiborlem4  38273  heiborlem6  38275  heiborlem10  38279  mapdhval  42308  hdmap1fval  42380  hdmap1vallem  42381  hdmap1val  42382  hdmap1cbv  42386  sticksstones10  42732  sticksstones12a  42734  fsuppind  43132  irrapxlem4  43362  clsk1indlem0  44577  clsk1indlem2  44578  clsk1indlem3  44579  clsk1indlem4  44580  clsk1indlem1  44581  dirkerval2  46628  dirkeritg  46636  dirkercncf  46641  fourierdlem29  46670  fourierdlem37  46678  fourierdlem62  46702  fourierdlem79  46719  fourierdlem81  46721  fourierdlem82  46722  fourierdlem92  46732  fourierdlem96  46736  fourierdlem97  46737  fourierdlem98  46738  fourierdlem99  46739  fourierdlem105  46745  fourierdlem108  46748  fourierdlem110  46750  fourierdlem112  46752  fourierdlem113  46753  fouriersw  46765  etransclem24  46792  etransclem25  46793  etransclem31  46799  etransclem35  46803  etransclem37  46805  sge0val  46900  nnfoctbdjlem  46989  nnfoctbdj  46990  ovnval  47075  ovnval2  47079  ovnval2b  47086  hsphoif  47110  hoidmvval  47111  hsphoival  47113  hoidmv1lelem1  47125  hoidmv1lelem2  47126  hoidmv1lelem3  47127  hoidmv1le  47128  ovnhoi  47137  hoidifhspval  47142  hspmbllem2  47161  ovnsubadd2  47180  blenval  49153