Theorem ifbieq2d 4465

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ifcif 4439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-un 3871  df-if 4440

This theorem is referenced by:  tz7.44-2  8143  tz7.44-3  8144  oev  8241  cantnfp1lem1  9293  cantnfp1lem3  9295  fin23lem12  9945  fin23lem33  9959  axcc2  10051  ttukeylem3  10125  ttukey2g  10130  canthp1lem2  10267  canthp1  10268  xnegeq  12797  xaddval  12813  xmulval  12815  expval  13637  cshfn  14355  ofccat  14532  relexpsucnnr  14588  sgnval  14651  sadcp1  16014  smupp1  16039  gcdval  16055  gcdass  16107  lcmval  16149  lcmass  16171  lcmfval  16178  lcmf0val  16179  lcmfpr  16184  iserodd  16388  pcval  16397  vdwlem6  16539  ramub1lem2  16580  ramcl  16582  mulgval  18492  symgextfv  18810  symgfixfo  18831  odfval  18924  odval  18926  submod  18958  gexval  18967  znval  20500  fvmptnn04if  21746  cpmadumatpoly  21780  cayleyhamilton  21787  cayleyhamiltonALT  21788  ptcmplem2  22950  iccpnfhmeo  23842  pcopt  23919  ioombl1  24459  ioorval  24471  uniioombllem6  24485  itg1addlem3  24595  itg2uba  24641  limcfval  24769  limcmpt  24780  limcco  24790  dvcobr  24843  ig1pval  25070  abelthlem9  25332  logtayllem  25547  logtayl  25548  leibpilem2  25824  rlimcnp2  25849  efrlim  25852  igamval  25929  muval  26014  lgsval  26182  lgsfval  26183  lgsval2lem  26188  rpvmasum2  26393  padicval  26498  padicabv  26511  axlowdimlem15  27047  axlowdim  27052  eupth2lem3lem3  28313  eupth2  28322  eucrct2eupth  28328  psgnfzto1stlem  31086  sgnsv  31146  sgnsval  31147  madjusmdetlem2  31492  madjusmdet  31495  xrge0iifcv  31598  xrge0iifhom  31601  xrge0tmd  31609  xrge0tmdALT  31610  signspval  32243  ex-sategoelel  33096  rdgprc0  33488  dfrdg2  33490  dfrdg4  33990  csbrdgg  35237  finxpeq1  35294  finxpreclem3  35301  poimirlem1  35515  poimirlem7  35521  poimirlem10  35524  poimirlem11  35525  itg2addnclem  35565  itg2addnclem3  35567  itg2addnc  35568  fdc  35640  heiborlem4  35709  heiborlem6  35711  heiborlem10  35715  mapdhval  39475  hdmap1fval  39547  hdmap1vallem  39548  hdmap1val  39549  hdmap1cbv  39553  sticksstones10  39833  sticksstones12a  39835  metakunt3  39849  metakunt4  39850  metakunt6  39852  metakunt7  39853  metakunt8  39854  metakunt10  39856  metakunt11  39857  metakunt12  39858  metakunt20  39866  metakunt21  39867  metakunt22  39868  fsuppind  39989  irrapxlem4  40350  clsk1indlem0  41328  clsk1indlem2  41329  clsk1indlem3  41330  clsk1indlem4  41331  clsk1indlem1  41332  dirkerval2  43310  dirkeritg  43318  dirkercncf  43323  fourierdlem29  43352  fourierdlem37  43360  fourierdlem62  43384  fourierdlem79  43401  fourierdlem81  43403  fourierdlem82  43404  fourierdlem92  43414  fourierdlem96  43418  fourierdlem97  43419  fourierdlem98  43420  fourierdlem99  43421  fourierdlem105  43427  fourierdlem108  43430  fourierdlem110  43432  fourierdlem112  43434  fourierdlem113  43435  fouriersw  43447  etransclem24  43474  etransclem25  43475  etransclem31  43481  etransclem35  43485  etransclem37  43487  sge0val  43579  nnfoctbdjlem  43668  nnfoctbdj  43669  ovnval  43754  ovnval2  43758  ovnval2b  43765  hsphoif  43789  hoidmvval  43790  hsphoival  43792  hoidmv1lelem1  43804  hoidmv1lelem2  43805  hoidmv1lelem3  43806  hoidmv1le  43807  ovnhoi  43816  hoidifhspval  43821  hspmbllem2  43840  ovnsubadd2  43859  blenval  45590