Theorem ifbieq12d 4453

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 4448	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐴, 𝐵))
3		ifbieq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4		ifbieq12d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	ifeq12d 4446	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))
6	2, 5	eqtrd 2771	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = if(𝜒, 𝐶, 𝐷))

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

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 2018  ax-8 2114  ax-9 2122  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 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-un 3858  df-if 4426

This theorem is referenced by:  csbif  4482  csbopg  4788  tz7.44-2  8121  tz7.44-3  8122  boxcutc  8600  unxpdomlem1  8858  updjudhcoinlf  9513  updjudhcoinrg  9514  dfac12lem1  9722  dfac12r  9725  fin23lem12  9910  fin23lem33  9924  ttukeylem3  10090  ttukey2g  10095  xaddval  12778  seqf1olem2  13581  expval  13602  ccatfval  14093  ccatval1  14098  ccatval1OLD  14099  ccatval2  14100  ccatalpha  14115  relexpsucnnr  14553  ruclem1  15755  eucalgval2  16101  setsstruct  16705  ressval  16735  gsumvalx  18102  gsumpropd  18104  gsumpropd2lem  18105  gsumress  18108  mulgval  18446  pmtrfv  18798  xrsdsval  20361  mvrfval  20899  selvfval  21031  marrepeval  21414  marepveval  21419  mdetunilem9  21471  madutpos  21493  madugsum  21494  minmar1eval  21500  symgmatr01lem  21504  symgmatr01  21505  gsummatr01lem3  21508  gsummatr01lem4  21509  gsummatr01  21510  ptcmplem3  22905  xrhmeo  23797  phtpycc  23842  pcovalg  23863  pcocn  23868  pcohtpylem  23870  pcoass  23875  pcorevlem  23877  ovolunlem1a  24347  ovolunlem1  24348  ioombl1  24413  mbfmax  24500  mbfpos  24502  mbfi1fseqlem2  24568  mbfi1fseq  24573  ditgeq1  24699  ditgeq2  24700  ig1pval  25024  cxpval  25506  lgamgulmlem4  25868  lgamgulmlem5  25869  musumsum  26028  muinv  26029  lgsval  26136  gausslemma2dlem1a  26200  gausslemma2dlem2  26202  gausslemma2dlem3  26203  gausslemma2dlem4  26204  vtxval  27045  iedgval  27046  crctcshwlkn0lem2  27849  crctcshwlkn0lem3  27850  crctcshlem4  27858  crctcsh  27862  clwlkclwwlklem2fv1  28032  eucrct2eupth  28282  psgnfzto1stlem  31040  resvval  31199  smatrcl  31414  smatlem  31415  madjusmdetlem2  31446  madjusmdet  31449  ballotlemsv  32142  ballotlemsf1o  32146  plymulx0  32192  mrsubcv  33139  mrsubrn  33142  rdgprc0  33439  dfrdg2  33441  csbrdgg  35186  csbfinxpg  35245  finxpreclem3  35250  poimirlem2  35465  poimirlem23  35486  poimirlem24  35487  poimirlem27  35490  itg2addnclem3  35516  itgaddnclem2  35522  ftc1anclem5  35540  cdleme27b  38068  cdleme29b  38075  cdleme31sn  38080  cdleme31fv  38090  cdleme40v  38169  dihffval  38930  dihfval  38931  dihval  38932  metakunt3  39790  metakunt4  39791  metakunt6  39793  metakunt7  39794  metakunt8  39795  metakunt10  39797  metakunt11  39798  metakunt12  39799  metakunt20  39807  metakunt21  39808  metakunt22  39809  metakunt32  39819  prjspnfv01  40110  prjspner01  40111  prjspner1  40112  aomclem8  40530  mnringvald  41445  icccncfext  43046  dvnxpaek  43101  fourierdlem103  43368  fourierdlem104  43369  ioorrnopn  43464  ioorrnopnxr  43466  hsphoival  43735  sge0hsphoire  43745  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem3  43753  hoidmvlelem4  43754  hoidmvlelem5  43755  hoidifhspval3  43775  hspmbllem2  43783  ovolval4  43807  afv2eq12d  44322