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 2764	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜒, 𝐶, 𝐵))

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

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 3406  df-v 3449  df-un 3919  df-if 4489

This theorem is referenced by:  tz7.44-2  8375  tz7.44-3  8376  oev  8478  cantnfp1lem1  9631  cantnfp1lem3  9633  ttrclselem2  9679  fin23lem12  10284  fin23lem33  10298  axcc2  10390  ttukeylem3  10464  ttukey2g  10469  canthp1lem2  10606  canthp1  10607  xnegeq  13167  xaddval  13183  xmulval  13185  expval  14028  cshfn  14755  ofccat  14935  relexpsucnnr  14991  sgnval  15054  sadcp1  16425  smupp1  16450  gcdval  16466  gcdass  16517  lcmval  16562  lcmass  16584  lcmfval  16591  lcmf0val  16592  lcmfpr  16597  iserodd  16806  pcval  16815  vdwlem6  16957  ramub1lem2  16998  ramcl  17000  mulgval  19003  symgextfv  19348  symgfixfo  19369  odfval  19462  odval  19464  submod  19499  gexval  19508  znval  21445  fvmptnn04if  22736  cpmadumatpoly  22770  cayleyhamilton  22777  cayleyhamiltonALT  22778  ptcmplem2  23940  iccpnfhmeo  24843  pcopt  24922  ioombl1  25463  ioorval  25475  uniioombllem6  25489  itg1addlem3  25599  itg2uba  25644  limcfval  25773  limcmpt  25784  limcco  25794  dvcobr  25849  dvcobrOLD  25850  ig1pval  26081  abelthlem9  26350  logtayllem  26568  logtayl  26569  leibpilem2  26851  rlimcnp2  26876  efrlim  26879  efrlimOLD  26880  igamval  26957  muval  27042  lgsval  27212  lgsfval  27213  lgsval2lem  27218  rpvmasum2  27423  padicval  27528  padicabv  27541  expsval  28311  axlowdimlem15  28883  axlowdim  28888  eupth2lem3lem3  30159  eupth2  30168  eucrct2eupth  30174  psgnfzto1stlem  33057  sgnsv  33117  sgnsval  33118  madjusmdetlem2  33818  madjusmdet  33821  xrge0iifcv  33924  xrge0iifhom  33927  xrge0tmd  33935  xrge0tmdALT  33936  signspval  34543  ex-sategoelel  35408  rdgprc0  35781  dfrdg2  35783  dfrdg4  35939  csbrdgg  37317  finxpeq1  37374  finxpreclem3  37381  poimirlem1  37615  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  fdc  37739  heiborlem4  37808  heiborlem6  37810  heiborlem10  37814  mapdhval  41718  hdmap1fval  41790  hdmap1vallem  41791  hdmap1val  41792  hdmap1cbv  41796  sticksstones10  42143  sticksstones12a  42145  fsuppind  42578  irrapxlem4  42813  clsk1indlem0  44030  clsk1indlem2  44031  clsk1indlem3  44032  clsk1indlem4  44033  clsk1indlem1  44034  dirkerval2  46092  dirkeritg  46100  dirkercncf  46105  fourierdlem29  46134  fourierdlem37  46142  fourierdlem62  46166  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem92  46196  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem105  46209  fourierdlem108  46212  fourierdlem110  46214  fourierdlem112  46216  fourierdlem113  46217  fouriersw  46229  etransclem24  46256  etransclem25  46257  etransclem31  46263  etransclem35  46267  etransclem37  46269  sge0val  46364  nnfoctbdjlem  46453  nnfoctbdj  46454  ovnval  46539  ovnval2  46543  ovnval2b  46550  hsphoif  46574  hoidmvval  46575  hsphoival  46577  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmv1le  46592  ovnhoi  46601  hoidifhspval  46606  hspmbllem2  46625  ovnsubadd2  46644  blenval  48560