Theorem ifbieq2d 4515

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3911  df-if 4489

This theorem is referenced by:  tz7.44-2  8395  tz7.44-3  8396  oev  8500  cantnfp1lem1  9648  cantnfp1lem3  9650  ttrclselem2  9696  fin23lem12  10316  fin23lem33  10330  axcc2  10422  ttukeylem3  10496  ttukey2g  10501  canthp1lem2  10639  canthp1  10640  xnegeq  13234  xaddval  13250  xmulval  13252  expval  14101  cshfn  14829  ofccat  15008  relexpsucnnr  15064  sgnval  15127  sadcp1  16514  smupp1  16539  gcdval  16555  gcdass  16606  lcmval  16651  lcmass  16673  lcmfval  16680  lcmf0val  16681  lcmfpr  16686  iserodd  16896  pcval  16905  vdwlem6  17047  ramub1lem2  17088  ramcl  17090  mulgval  19138  symgextfv  19489  symgfixfo  19510  odfval  19603  odval  19605  submod  19640  gexval  19649  znval  21666  fvmptnn04if  22987  cpmadumatpoly  23021  cayleyhamilton  23028  cayleyhamiltonALT  23029  ptcmplem2  24191  iccpnfhmeo  25085  pcopt  25162  ioombl1  25702  ioorval  25714  uniioombllem6  25728  itg1addlem3  25838  itg2uba  25883  limcfval  26012  limcmpt  26023  limcco  26033  dvcobr  26086  ig1pval  26314  abelthlem9  26584  logtayllem  26805  logtayl  26806  leibpilem2  27087  rlimcnp2  27112  efrlim  27115  igamval  27192  muval  27277  lgsval  27446  lgsfval  27447  lgsval2lem  27452  rpvmasum2  27657  padicval  27762  padicabv  27775  expsval  28599  axlowdimlem15  29287  axlowdim  29292  eupth2lem3lem3  30562  eupth2  30571  eucrct2eupth  30577  psgnfzto1stlem  33401  sgnsv  33461  sgnsval  33462  madjusmdetlem2  34199  madjusmdet  34202  xrge0iifcv  34305  xrge0iifhom  34308  xrge0tmd  34316  xrge0tmdALT  34317  signspval  34920  ex-sategoelel  35894  rdgprc0  36264  dfrdg2  36266  dfrdg4  36424  csbrdgg  37956  finxpeq1  38013  finxpreclem3  38020  poimirlem1  38253  poimirlem7  38259  poimirlem10  38262  poimirlem11  38263  itg2addnclem  38303  itg2addnclem3  38305  itg2addnc  38306  fdc  38377  heiborlem4  38446  heiborlem6  38448  heiborlem10  38452  mapdhval  42479  hdmap1fval  42551  hdmap1vallem  42552  hdmap1val  42553  hdmap1cbv  42557  sticksstones10  42903  sticksstones12a  42905  fsuppind  43305  irrapxlem4  43535  clsk1indlem0  44750  clsk1indlem2  44751  clsk1indlem3  44752  clsk1indlem4  44753  clsk1indlem1  44754  dirkerval2  46791  dirkeritg  46799  dirkercncf  46804  fourierdlem29  46833  fourierdlem37  46841  fourierdlem62  46865  fourierdlem79  46882  fourierdlem81  46884  fourierdlem82  46885  fourierdlem92  46895  fourierdlem96  46899  fourierdlem97  46900  fourierdlem98  46901  fourierdlem99  46902  fourierdlem105  46908  fourierdlem108  46911  fourierdlem110  46913  fourierdlem112  46915  fourierdlem113  46916  fouriersw  46928  etransclem24  46955  etransclem25  46956  etransclem31  46962  etransclem35  46966  etransclem37  46968  sge0val  47063  nnfoctbdjlem  47152  nnfoctbdj  47153  ovnval  47238  ovnval2  47242  ovnval2b  47249  hsphoif  47273  hoidmvval  47274  hsphoival  47276  hoidmv1lelem1  47288  hoidmv1lelem2  47289  hoidmv1lelem3  47290  hoidmv1le  47291  ovnhoi  47300  hoidifhspval  47305  hspmbllem2  47324  ovnsubadd2  47343  blenval  49334