Theorem ifbieq2d 4304

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

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  ifcif 4279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-un 3774  df-if 4280

This theorem is referenced by:  tz7.44-2  7739  tz7.44-3  7740  oev  7831  cantnfp1lem1  8822  cantnfp1lem3  8824  fin23lem12  9438  fin23lem33  9452  axcc2  9544  ttukeylem3  9618  ttukey2g  9623  canthp1lem2  9760  canthp1  9761  xnegeq  12256  xaddval  12272  xmulval  12274  expval  13085  cshfn  13760  ofccat  13933  relexpsucnnr  13988  sgnval  14051  sadcp1  15396  smupp1  15421  gcdval  15437  gcdass  15483  lcmval  15524  lcmass  15546  lcmfval  15553  lcmf0val  15554  lcmfpr  15559  iserodd  15757  pcval  15766  vdwlem6  15907  ramub1lem2  15948  ramcl  15950  mulgval  17748  symgextfv  18039  symgfixfo  18060  odval  18154  submod  18185  gexval  18194  znval  20091  fvmptnn04if  20867  cpmadumatpoly  20901  cayleyhamilton  20908  cayleyhamiltonALT  20909  ptcmplem2  22070  iccpnfhmeo  22957  pcopt  23034  ioombl1  23543  ioorval  23555  uniioombllem6  23569  itg1addlem3  23679  itg2uba  23724  limcfval  23850  limcmpt  23861  limcco  23871  dvcobr  23923  ig1pval  24146  abelthlem9  24408  logtayllem  24619  logtayl  24620  leibpilem2  24882  rlimcnp2  24907  efrlim  24910  igamval  24987  muval  25072  lgsval  25240  lgsfval  25241  lgsval2lem  25246  rpvmasum2  25415  padicval  25520  padicabv  25533  axlowdimlem15  26050  axlowdim  26055  eupth2lem3lem3  27403  eupth2  27412  eucrct2eupth  27418  sgnsv  30052  sgnsval  30053  psgnfzto1stlem  30175  madjusmdetlem2  30219  madjusmdet  30222  xrge0iifcv  30305  xrge0iifhom  30308  xrge0tmdOLD  30316  xrge0tmd  30317  signspval  30954  rdgprc0  32019  dfrdg2  32021  dfrdg4  32379  csbrdgg  33492  finxpeq1  33539  finxpreclem3  33546  poimirlem1  33723  poimirlem7  33729  poimirlem10  33732  poimirlem11  33733  itg2addnclem  33773  itg2addnclem3  33775  itg2addnc  33776  fdc  33852  heiborlem4  33924  heiborlem6  33926  heiborlem10  33930  mapdhval  37505  hdmap1fval  37577  hdmap1vallem  37578  hdmap1val  37579  hdmap1cbv  37583  irrapxlem4  37891  clsk1indlem0  38839  clsk1indlem2  38840  clsk1indlem3  38841  clsk1indlem4  38842  clsk1indlem1  38843  dirkerval2  40790  dirkeritg  40798  dirkercncf  40803  fourierdlem29  40832  fourierdlem37  40840  fourierdlem62  40864  fourierdlem79  40881  fourierdlem81  40883  fourierdlem82  40884  fourierdlem92  40894  fourierdlem96  40898  fourierdlem97  40899  fourierdlem98  40900  fourierdlem99  40901  fourierdlem105  40907  fourierdlem108  40910  fourierdlem110  40912  fourierdlem112  40914  fourierdlem113  40915  fouriersw  40927  etransclem24  40954  etransclem25  40955  etransclem31  40961  etransclem35  40965  etransclem37  40967  sge0val  41062  nnfoctbdjlem  41151  nnfoctbdj  41152  ovnval  41237  ovnval2  41241  ovnval2b  41248  hsphoif  41272  hoidmvval  41273  hsphoival  41275  hoidmv1lelem1  41287  hoidmv1lelem2  41288  hoidmv1lelem3  41289  hoidmv1le  41290  ovnhoi  41299  hoidifhspval  41304  hspmbllem2  41323  ovnsubadd2  41342  blenval  42933