Theorem ifbieq2d 4505

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-un 3910  df-if 4479

This theorem is referenced by:  tz7.44-2  8336  tz7.44-3  8337  oev  8439  cantnfp1lem1  9593  cantnfp1lem3  9595  ttrclselem2  9641  fin23lem12  10244  fin23lem33  10258  axcc2  10350  ttukeylem3  10424  ttukey2g  10429  canthp1lem2  10566  canthp1  10567  xnegeq  13127  xaddval  13143  xmulval  13145  expval  13988  cshfn  14714  ofccat  14894  relexpsucnnr  14950  sgnval  15013  sadcp1  16384  smupp1  16409  gcdval  16425  gcdass  16476  lcmval  16521  lcmass  16543  lcmfval  16550  lcmf0val  16551  lcmfpr  16556  iserodd  16765  pcval  16774  vdwlem6  16916  ramub1lem2  16957  ramcl  16959  mulgval  18968  symgextfv  19315  symgfixfo  19336  odfval  19429  odval  19431  submod  19466  gexval  19475  znval  21460  fvmptnn04if  22752  cpmadumatpoly  22786  cayleyhamilton  22793  cayleyhamiltonALT  22794  ptcmplem2  23956  iccpnfhmeo  24859  pcopt  24938  ioombl1  25479  ioorval  25491  uniioombllem6  25505  itg1addlem3  25615  itg2uba  25660  limcfval  25789  limcmpt  25800  limcco  25810  dvcobr  25865  dvcobrOLD  25866  ig1pval  26097  abelthlem9  26366  logtayllem  26584  logtayl  26585  leibpilem2  26867  rlimcnp2  26892  efrlim  26895  efrlimOLD  26896  igamval  26973  muval  27058  lgsval  27228  lgsfval  27229  lgsval2lem  27234  rpvmasum2  27439  padicval  27544  padicabv  27557  expsval  28335  axlowdimlem15  28919  axlowdim  28924  eupth2lem3lem3  30192  eupth2  30201  eucrct2eupth  30207  psgnfzto1stlem  33055  sgnsv  33115  sgnsval  33116  madjusmdetlem2  33797  madjusmdet  33800  xrge0iifcv  33903  xrge0iifhom  33906  xrge0tmd  33914  xrge0tmdALT  33915  signspval  34522  ex-sategoelel  35396  rdgprc0  35769  dfrdg2  35771  dfrdg4  35927  csbrdgg  37305  finxpeq1  37362  finxpreclem3  37369  poimirlem1  37603  poimirlem7  37609  poimirlem10  37612  poimirlem11  37613  itg2addnclem  37653  itg2addnclem3  37655  itg2addnc  37656  fdc  37727  heiborlem4  37796  heiborlem6  37798  heiborlem10  37802  mapdhval  41706  hdmap1fval  41778  hdmap1vallem  41779  hdmap1val  41780  hdmap1cbv  41784  sticksstones10  42131  sticksstones12a  42133  fsuppind  42566  irrapxlem4  42801  clsk1indlem0  44017  clsk1indlem2  44018  clsk1indlem3  44019  clsk1indlem4  44020  clsk1indlem1  44021  dirkerval2  46079  dirkeritg  46087  dirkercncf  46092  fourierdlem29  46121  fourierdlem37  46129  fourierdlem62  46153  fourierdlem79  46170  fourierdlem81  46172  fourierdlem82  46173  fourierdlem92  46183  fourierdlem96  46187  fourierdlem97  46188  fourierdlem98  46189  fourierdlem99  46190  fourierdlem105  46196  fourierdlem108  46199  fourierdlem110  46201  fourierdlem112  46203  fourierdlem113  46204  fouriersw  46216  etransclem24  46243  etransclem25  46244  etransclem31  46250  etransclem35  46254  etransclem37  46256  sge0val  46351  nnfoctbdjlem  46440  nnfoctbdj  46441  ovnval  46526  ovnval2  46530  ovnval2b  46537  hsphoif  46561  hoidmvval  46562  hsphoival  46564  hoidmv1lelem1  46576  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmv1le  46579  ovnhoi  46588  hoidifhspval  46593  hspmbllem2  46612  ovnsubadd2  46631  blenval  48560