Theorem ifbieq12d 4559

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-un 3968  df-if 4532

This theorem is referenced by:  csbif  4588  csbopg  4896  tz7.44-2  8446  tz7.44-3  8447  boxcutc  8980  unxpdomlem1  9284  ttrcltr  9754  updjudhcoinlf  9970  updjudhcoinrg  9971  dfac12lem1  10182  dfac12r  10185  fin23lem12  10369  fin23lem33  10383  ttukeylem3  10549  ttukey2g  10554  xaddval  13262  seqf1olem2  14080  expval  14101  ccatfval  14608  ccatval1  14612  ccatval2  14613  ccatalpha  14628  relexpsucnnr  15061  ruclem1  16264  eucalgval2  16615  setsstruct  17210  ressval  17277  gsumvalx  18702  gsumpropd  18704  gsumpropd2lem  18705  gsumress  18708  mulgval  19102  pmtrfv  19485  xrsdsval  21446  mvrfval  22019  selvfval  22156  marrepeval  22585  marepveval  22590  mdetunilem9  22642  madutpos  22664  madugsum  22665  minmar1eval  22671  symgmatr01lem  22675  symgmatr01  22676  gsummatr01lem3  22679  gsummatr01lem4  22680  gsummatr01  22681  ptcmplem3  24078  xrhmeo  24991  phtpycc  25037  pcovalg  25059  pcocn  25064  pcohtpylem  25066  pcoass  25071  pcorevlem  25073  ovolunlem1a  25545  ovolunlem1  25546  ioombl1  25611  mbfmax  25698  mbfpos  25700  mbfi1fseqlem2  25766  mbfi1fseq  25771  ditgeq1  25898  ditgeq2  25899  ig1pval  26230  cxpval  26721  lgamgulmlem4  27090  lgamgulmlem5  27091  musumsum  27250  muinv  27251  lgsval  27360  gausslemma2dlem1a  27424  gausslemma2dlem2  27426  gausslemma2dlem3  27427  gausslemma2dlem4  27428  abssval  28278  expsval  28423  vtxval  29032  iedgval  29033  crctcshwlkn0lem2  29841  crctcshwlkn0lem3  29842  crctcshlem4  29850  crctcsh  29854  clwlkclwwlklem2fv1  30024  eucrct2eupth  30274  ccatws1f1o  32921  psgnfzto1stlem  33103  resvval  33333  smatrcl  33757  smatlem  33758  madjusmdetlem2  33789  madjusmdet  33792  ballotlemsv  34491  ballotlemsf1o  34495  plymulx0  34541  mrsubcv  35495  mrsubrn  35498  rdgprc0  35775  dfrdg2  35777  ditgeq123dv  36204  cbvditgdavw2  36281  csbrdgg  37312  csbfinxpg  37371  finxpreclem3  37376  poimirlem2  37609  poimirlem23  37630  poimirlem24  37631  poimirlem27  37634  itg2addnclem3  37660  itgaddnclem2  37666  ftc1anclem5  37684  cdleme27b  40351  cdleme29b  40358  cdleme31sn  40363  cdleme31fv  40373  cdleme40v  40452  dihffval  41213  dihfval  41214  dihval  41215  metakunt3  42189  metakunt4  42190  metakunt6  42192  metakunt7  42193  metakunt8  42194  metakunt10  42196  metakunt11  42197  metakunt12  42198  metakunt20  42206  metakunt21  42207  metakunt22  42208  metakunt32  42218  selvvvval  42572  prjspnfv01  42611  prjspner01  42612  prjspner1  42613  aomclem8  43050  mnringvald  44204  icccncfext  45843  dvnxpaek  45898  fourierdlem103  46165  fourierdlem104  46166  ioorrnopn  46261  ioorrnopnxr  46263  hsphoival  46535  sge0hsphoire  46545  hoidmvlelem1  46551  hoidmvlelem2  46552  hoidmvlelem3  46553  hoidmvlelem4  46554  hoidmvlelem5  46555  hoidifhspval3  46575  hspmbllem2  46583  ovolval4  46607  afv2eq12d  47165