Theorem ifbieq2d 4502

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-un 3907  df-if 4476

This theorem is referenced by:  tz7.44-2  8326  tz7.44-3  8327  oev  8429  cantnfp1lem1  9568  cantnfp1lem3  9570  ttrclselem2  9616  fin23lem12  10222  fin23lem33  10236  axcc2  10328  ttukeylem3  10402  ttukey2g  10407  canthp1lem2  10544  canthp1  10545  xnegeq  13106  xaddval  13122  xmulval  13124  expval  13970  cshfn  14697  ofccat  14876  relexpsucnnr  14932  sgnval  14995  sadcp1  16366  smupp1  16391  gcdval  16407  gcdass  16458  lcmval  16503  lcmass  16525  lcmfval  16532  lcmf0val  16533  lcmfpr  16538  iserodd  16747  pcval  16756  vdwlem6  16898  ramub1lem2  16939  ramcl  16941  mulgval  18984  symgextfv  19331  symgfixfo  19352  odfval  19445  odval  19447  submod  19482  gexval  19491  znval  21473  fvmptnn04if  22765  cpmadumatpoly  22799  cayleyhamilton  22806  cayleyhamiltonALT  22807  ptcmplem2  23969  iccpnfhmeo  24871  pcopt  24950  ioombl1  25491  ioorval  25503  uniioombllem6  25517  itg1addlem3  25627  itg2uba  25672  limcfval  25801  limcmpt  25812  limcco  25822  dvcobr  25877  dvcobrOLD  25878  ig1pval  26109  abelthlem9  26378  logtayllem  26596  logtayl  26597  leibpilem2  26879  rlimcnp2  26904  efrlim  26907  efrlimOLD  26908  igamval  26985  muval  27070  lgsval  27240  lgsfval  27241  lgsval2lem  27246  rpvmasum2  27451  padicval  27556  padicabv  27569  expsval  28349  axlowdimlem15  28935  axlowdim  28940  eupth2lem3lem3  30208  eupth2  30217  eucrct2eupth  30223  psgnfzto1stlem  33067  sgnsv  33127  sgnsval  33128  madjusmdetlem2  33839  madjusmdet  33842  xrge0iifcv  33945  xrge0iifhom  33948  xrge0tmd  33956  xrge0tmdALT  33957  signspval  34563  ex-sategoelel  35463  rdgprc0  35833  dfrdg2  35835  dfrdg4  35991  csbrdgg  37369  finxpeq1  37426  finxpreclem3  37433  poimirlem1  37667  poimirlem7  37673  poimirlem10  37676  poimirlem11  37677  itg2addnclem  37717  itg2addnclem3  37719  itg2addnc  37720  fdc  37791  heiborlem4  37860  heiborlem6  37862  heiborlem10  37866  mapdhval  41769  hdmap1fval  41841  hdmap1vallem  41842  hdmap1val  41843  hdmap1cbv  41847  sticksstones10  42194  sticksstones12a  42196  fsuppind  42629  irrapxlem4  42864  clsk1indlem0  44080  clsk1indlem2  44081  clsk1indlem3  44082  clsk1indlem4  44083  clsk1indlem1  44084  dirkerval2  46138  dirkeritg  46146  dirkercncf  46151  fourierdlem29  46180  fourierdlem37  46188  fourierdlem62  46212  fourierdlem79  46229  fourierdlem81  46231  fourierdlem82  46232  fourierdlem92  46242  fourierdlem96  46246  fourierdlem97  46247  fourierdlem98  46248  fourierdlem99  46249  fourierdlem105  46255  fourierdlem108  46258  fourierdlem110  46260  fourierdlem112  46262  fourierdlem113  46263  fouriersw  46275  etransclem24  46302  etransclem25  46303  etransclem31  46309  etransclem35  46313  etransclem37  46315  sge0val  46410  nnfoctbdjlem  46499  nnfoctbdj  46500  ovnval  46585  ovnval2  46589  ovnval2b  46596  hsphoif  46620  hoidmvval  46621  hsphoival  46623  hoidmv1lelem1  46635  hoidmv1lelem2  46636  hoidmv1lelem3  46637  hoidmv1le  46638  ovnhoi  46647  hoidifhspval  46652  hspmbllem2  46671  ovnsubadd2  46690  blenval  48609