Theorem ifbieq12d 4063

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-un 3545  df-if 4037

This theorem is referenced by:  csbif  4088  csbopg  4358  tz7.44-2  7390  tz7.44-3  7391  boxcutc  7837  unxpdomlem1  8049  dfac12lem1  8848  dfac12r  8851  fin23lem12  9036  fin23lem33  9050  ttukeylem3  9216  ttukey2g  9221  xaddval  11928  seqf1olem2  12703  expval  12724  ccatfval  13211  ccatval1  13214  ccatval2  13215  ccatalpha  13228  relexpsucnnr  13613  ruclem1  14799  eucalgval2  15132  ressval  15754  gsumvalx  17093  gsumpropd  17095  gsumpropd2lem  17096  gsumress  17099  mulgval  17366  pmtrfv  17695  mvrfval  19241  xrsdsval  19609  marrepeval  20188  marepveval  20193  mdetunilem9  20245  madutpos  20267  madugsum  20268  minmar1eval  20274  symgmatr01lem  20278  symgmatr01  20279  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  ptcmplem3  21668  xrhmeo  22553  phtpycc  22598  pcovalg  22620  pcocn  22625  pcohtpylem  22627  pcoass  22632  pcorevlem  22634  ovolunlem1a  23071  ovolunlem1  23072  ioombl1  23137  mbfmax  23222  mbfpos  23224  mbfi1fseqlem2  23289  mbfi1fseq  23294  ditgeq1  23418  ditgeq2  23419  ig1pval  23736  cxpval  24210  lgamgulmlem4  24558  lgamgulmlem5  24559  musumsum  24718  muinv  24719  lgsval  24826  gausslemma2dlem1a  24890  gausslemma2dlem2  24892  gausslemma2dlem3  24893  gausslemma2dlem4  24894  vtxval  25677  iedgval  25678  clwlkisclwwlklem2fv1  26310  resvval  29158  psgnfzto1stlem  29181  smatrcl  29190  smatlem  29191  madjusmdetlem2  29222  madjusmdet  29225  ballotlemsv  29898  ballotlemsf1o  29902  plymulx0  29950  mrsubcv  30661  mrsubrn  30664  rdgprc0  30943  dfrdg2  30945  csbrdgg  32351  csbfinxpg  32401  finxpreclem3  32406  poimirlem2  32581  poimirlem23  32602  poimirlem24  32603  poimirlem27  32606  itg2addnclem3  32633  itgaddnclem2  32639  ftc1anclem5  32659  cdleme27b  34674  cdleme29b  34681  cdleme31sn  34686  cdleme31fv  34696  cdleme40v  34775  dihffval  35537  dihfval  35538  dihval  35539  aomclem8  36649  ifeq123d  38231  icccncfext  38773  dvnxpaek  38832  ioorrnopn  39201  ioorrnopnxr  39203  hsphoival  39469  sge0hsphoire  39479  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvlelem5  39489  hoidifhspval3  39509  hspmbllem2  39517  ovolval4  39541  crctcsh1wlkn0lem2  41014  crctcsh1wlkn0lem3  41015  crctcshlem4  41023  crctcsh  41027  clwlkclwwlklem2fv1  41204  eucrct2eupth  41413