Theorem ifbieq2d 4488

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-un 3895  df-if 4462

This theorem is referenced by:  tz7.44-2  8343  tz7.44-3  8344  oev  8446  cantnfp1lem1  9597  cantnfp1lem3  9599  ttrclselem2  9645  fin23lem12  10251  fin23lem33  10265  axcc2  10357  ttukeylem3  10431  ttukey2g  10436  canthp1lem2  10574  canthp1  10575  xnegeq  13157  xaddval  13173  xmulval  13175  expval  14023  cshfn  14750  ofccat  14929  relexpsucnnr  14985  sgnval  15048  sadcp1  16422  smupp1  16447  gcdval  16463  gcdass  16514  lcmval  16559  lcmass  16581  lcmfval  16588  lcmf0val  16589  lcmfpr  16594  iserodd  16804  pcval  16813  vdwlem6  16955  ramub1lem2  16996  ramcl  16998  mulgval  19045  symgextfv  19391  symgfixfo  19412  odfval  19505  odval  19507  submod  19542  gexval  19551  znval  21517  fvmptnn04if  22839  cpmadumatpoly  22873  cayleyhamilton  22880  cayleyhamiltonALT  22881  ptcmplem2  24043  iccpnfhmeo  24937  pcopt  25014  ioombl1  25554  ioorval  25566  uniioombllem6  25580  itg1addlem3  25690  itg2uba  25735  limcfval  25864  limcmpt  25875  limcco  25885  dvcobr  25938  ig1pval  26166  abelthlem9  26430  logtayllem  26648  logtayl  26649  leibpilem2  26930  rlimcnp2  26955  efrlim  26958  igamval  27035  muval  27120  lgsval  27289  lgsfval  27290  lgsval2lem  27295  rpvmasum2  27500  padicval  27605  padicabv  27618  expsval  28442  axlowdimlem15  29050  axlowdim  29055  eupth2lem3lem3  30325  eupth2  30334  eucrct2eupth  30340  psgnfzto1stlem  33188  sgnsv  33248  sgnsval  33249  madjusmdetlem2  34019  madjusmdet  34022  xrge0iifcv  34125  xrge0iifhom  34128  xrge0tmd  34136  xrge0tmdALT  34137  signspval  34743  ex-sategoelel  35656  rdgprc0  36026  dfrdg2  36028  dfrdg4  36186  csbrdgg  37698  finxpeq1  37755  finxpreclem3  37762  poimirlem1  37995  poimirlem7  38001  poimirlem10  38004  poimirlem11  38005  itg2addnclem  38045  itg2addnclem3  38047  itg2addnc  38048  fdc  38119  heiborlem4  38188  heiborlem6  38190  heiborlem10  38194  mapdhval  42223  hdmap1fval  42295  hdmap1vallem  42296  hdmap1val  42297  hdmap1cbv  42301  sticksstones10  42647  sticksstones12a  42649  fsuppind  43047  irrapxlem4  43277  clsk1indlem0  44492  clsk1indlem2  44493  clsk1indlem3  44494  clsk1indlem4  44495  clsk1indlem1  44496  dirkerval2  46544  dirkeritg  46552  dirkercncf  46557  fourierdlem29  46586  fourierdlem37  46594  fourierdlem62  46618  fourierdlem79  46635  fourierdlem81  46637  fourierdlem82  46638  fourierdlem92  46648  fourierdlem96  46652  fourierdlem97  46653  fourierdlem98  46654  fourierdlem99  46655  fourierdlem105  46661  fourierdlem108  46664  fourierdlem110  46666  fourierdlem112  46668  fourierdlem113  46669  fouriersw  46681  etransclem24  46708  etransclem25  46709  etransclem31  46715  etransclem35  46719  etransclem37  46721  sge0val  46816  nnfoctbdjlem  46905  nnfoctbdj  46906  ovnval  46991  ovnval2  46995  ovnval2b  47002  hsphoif  47026  hoidmvval  47027  hsphoival  47029  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmv1lelem3  47043  hoidmv1le  47044  ovnhoi  47053  hoidifhspval  47058  hspmbllem2  47077  ovnsubadd2  47096  blenval  49069