Theorem ifbieq12d 4520

Description: Equivalence deduction for conditional operators. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
ifbieq12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq12d.2	⊢ (𝜑 → 𝐴 = 𝐶)
ifbieq12d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
ifbieq12d	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))

Proof of Theorem ifbieq12d

Step	Hyp	Ref	Expression
1		ifbieq12d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 4515	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3		ifbieq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4		ifbieq12d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	ifeq12d 4513	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
6	2, 5	eqtrd 2765	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-un 3922  df-if 4492

This theorem is referenced by:  csbif  4549  csbopg  4858  tz7.44-2  8378  tz7.44-3  8379  boxcutc  8917  unxpdomlem1  9204  ttrcltr  9676  updjudhcoinlf  9892  updjudhcoinrg  9893  dfac12lem1  10104  dfac12r  10107  fin23lem12  10291  fin23lem33  10305  ttukeylem3  10471  ttukey2g  10476  xaddval  13190  seqf1olem2  14014  expval  14035  ccatfval  14545  ccatval1  14549  ccatval2  14550  ccatalpha  14565  relexpsucnnr  14998  ruclem1  16206  eucalgval2  16558  setsstruct  17153  ressval  17210  gsumvalx  18610  gsumpropd  18612  gsumpropd2lem  18613  gsumress  18616  mulgval  19010  pmtrfv  19389  xrsdsval  21334  mvrfval  21897  selvfval  22028  marrepeval  22457  marepveval  22462  mdetunilem9  22514  madutpos  22536  madugsum  22537  minmar1eval  22543  symgmatr01lem  22547  symgmatr01  22548  gsummatr01lem3  22551  gsummatr01lem4  22552  gsummatr01  22553  ptcmplem3  23948  xrhmeo  24851  phtpycc  24897  pcovalg  24919  pcocn  24924  pcohtpylem  24926  pcoass  24931  pcorevlem  24933  ovolunlem1a  25404  ovolunlem1  25405  ioombl1  25470  mbfmax  25557  mbfpos  25559  mbfi1fseqlem2  25624  mbfi1fseq  25629  ditgeq1  25756  ditgeq2  25757  ig1pval  26088  cxpval  26580  lgamgulmlem4  26949  lgamgulmlem5  26950  musumsum  27109  muinv  27110  lgsval  27219  gausslemma2dlem1a  27283  gausslemma2dlem2  27285  gausslemma2dlem3  27286  gausslemma2dlem4  27287  abssval  28148  expsval  28318  vtxval  28934  iedgval  28935  crctcshwlkn0lem2  29748  crctcshwlkn0lem3  29749  crctcshlem4  29757  crctcsh  29761  clwlkclwwlklem2fv1  29931  eucrct2eupth  30181  ccatws1f1o  32880  psgnfzto1stlem  33064  resvval  33308  smatrcl  33793  smatlem  33794  madjusmdetlem2  33825  madjusmdet  33828  ballotlemsv  34508  ballotlemsf1o  34512  plymulx0  34545  mrsubcv  35504  mrsubrn  35507  rdgprc0  35788  dfrdg2  35790  ditgeq123dv  36216  cbvditgdavw2  36293  csbrdgg  37324  csbfinxpg  37383  finxpreclem3  37388  poimirlem2  37623  poimirlem23  37644  poimirlem24  37645  poimirlem27  37648  itg2addnclem3  37674  itgaddnclem2  37680  ftc1anclem5  37698  cdleme27b  40369  cdleme29b  40376  cdleme31sn  40381  cdleme31fv  40391  cdleme40v  40470  dihffval  41231  dihfval  41232  dihval  41233  selvvvval  42580  prjspnfv01  42619  prjspner01  42620  prjspner1  42621  aomclem8  43057  mnringvald  44209  icccncfext  45892  dvnxpaek  45947  fourierdlem103  46214  fourierdlem104  46215  ioorrnopn  46310  ioorrnopnxr  46312  hsphoival  46584  sge0hsphoire  46594  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hoidmvlelem5  46604  hoidifhspval3  46624  hspmbllem2  46632  ovolval4  46656  afv2eq12d  47220