Theorem ifbieq2d 4503

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-un 3903  df-if 4477

This theorem is referenced by:  tz7.44-2  8334  tz7.44-3  8335  oev  8437  cantnfp1lem1  9577  cantnfp1lem3  9579  ttrclselem2  9625  fin23lem12  10231  fin23lem33  10245  axcc2  10337  ttukeylem3  10411  ttukey2g  10416  canthp1lem2  10553  canthp1  10554  xnegeq  13110  xaddval  13126  xmulval  13128  expval  13974  cshfn  14701  ofccat  14880  relexpsucnnr  14936  sgnval  14999  sadcp1  16370  smupp1  16395  gcdval  16411  gcdass  16462  lcmval  16507  lcmass  16529  lcmfval  16536  lcmf0val  16537  lcmfpr  16542  iserodd  16751  pcval  16760  vdwlem6  16902  ramub1lem2  16943  ramcl  16945  mulgval  18988  symgextfv  19334  symgfixfo  19355  odfval  19448  odval  19450  submod  19485  gexval  19494  znval  21476  fvmptnn04if  22767  cpmadumatpoly  22801  cayleyhamilton  22808  cayleyhamiltonALT  22809  ptcmplem2  23971  iccpnfhmeo  24873  pcopt  24952  ioombl1  25493  ioorval  25505  uniioombllem6  25519  itg1addlem3  25629  itg2uba  25674  limcfval  25803  limcmpt  25814  limcco  25824  dvcobr  25879  dvcobrOLD  25880  ig1pval  26111  abelthlem9  26380  logtayllem  26598  logtayl  26599  leibpilem2  26881  rlimcnp2  26906  efrlim  26909  efrlimOLD  26910  igamval  26987  muval  27072  lgsval  27242  lgsfval  27243  lgsval2lem  27248  rpvmasum2  27453  padicval  27558  padicabv  27571  expsval  28351  axlowdimlem15  28938  axlowdim  28943  eupth2lem3lem3  30214  eupth2  30223  eucrct2eupth  30229  psgnfzto1stlem  33078  sgnsv  33138  sgnsval  33139  madjusmdetlem2  33864  madjusmdet  33867  xrge0iifcv  33970  xrge0iifhom  33973  xrge0tmd  33981  xrge0tmdALT  33982  signspval  34588  ex-sategoelel  35488  rdgprc0  35858  dfrdg2  35860  dfrdg4  36018  csbrdgg  37396  finxpeq1  37453  finxpreclem3  37460  poimirlem1  37684  poimirlem7  37690  poimirlem10  37693  poimirlem11  37694  itg2addnclem  37734  itg2addnclem3  37736  itg2addnc  37737  fdc  37808  heiborlem4  37877  heiborlem6  37879  heiborlem10  37883  mapdhval  41846  hdmap1fval  41918  hdmap1vallem  41919  hdmap1val  41920  hdmap1cbv  41924  sticksstones10  42271  sticksstones12a  42273  fsuppind  42711  irrapxlem4  42945  clsk1indlem0  44161  clsk1indlem2  44162  clsk1indlem3  44163  clsk1indlem4  44164  clsk1indlem1  44165  dirkerval2  46219  dirkeritg  46227  dirkercncf  46232  fourierdlem29  46261  fourierdlem37  46269  fourierdlem62  46293  fourierdlem79  46310  fourierdlem81  46312  fourierdlem82  46313  fourierdlem92  46323  fourierdlem96  46327  fourierdlem97  46328  fourierdlem98  46329  fourierdlem99  46330  fourierdlem105  46336  fourierdlem108  46339  fourierdlem110  46341  fourierdlem112  46343  fourierdlem113  46344  fouriersw  46356  etransclem24  46383  etransclem25  46384  etransclem31  46390  etransclem35  46394  etransclem37  46396  sge0val  46491  nnfoctbdjlem  46580  nnfoctbdj  46581  ovnval  46666  ovnval2  46670  ovnval2b  46677  hsphoif  46701  hoidmvval  46702  hsphoival  46704  hoidmv1lelem1  46716  hoidmv1lelem2  46717  hoidmv1lelem3  46718  hoidmv1le  46719  ovnhoi  46728  hoidifhspval  46733  hspmbllem2  46752  ovnsubadd2  46771  blenval  48699