Theorem ifbieq12d 4490

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-un 3895  df-if 4462

This theorem is referenced by:  csbif  4519  csbopg  4829  tz7.44-2  8343  tz7.44-3  8344  boxcutc  8886  unxpdomlem1  9163  ttrcltr  9635  updjudhcoinlf  9854  updjudhcoinrg  9855  dfac12lem1  10064  dfac12r  10067  fin23lem12  10251  fin23lem33  10265  ttukeylem3  10431  ttukey2g  10436  xaddval  13173  seqf1olem2  14002  expval  14023  ccatfval  14533  ccatval1  14537  ccatval2  14538  ccatalpha  14554  relexpsucnnr  14985  ruclem1  16196  eucalgval2  16548  setsstruct  17144  ressval  17201  gsumvalx  18642  gsumpropd  18644  gsumpropd2lem  18645  gsumress  18648  mulgval  19045  pmtrfv  19425  xrsdsval  21393  mvrfval  21962  selvfval  22102  selvvvval  22125  marrepeval  22553  marepveval  22558  mdetunilem9  22610  madutpos  22632  madugsum  22633  minmar1eval  22639  symgmatr01lem  22643  symgmatr01  22644  gsummatr01lem3  22647  gsummatr01lem4  22648  gsummatr01  22649  ptcmplem3  24044  xrhmeo  24938  phtpycc  24983  pcovalg  25004  pcocn  25009  pcohtpylem  25011  pcoass  25016  pcorevlem  25018  ovolunlem1a  25488  ovolunlem1  25489  ioombl1  25554  mbfmax  25641  mbfpos  25643  mbfi1fseqlem2  25708  mbfi1fseq  25713  ditgeq1  25840  ditgeq2  25841  ig1pval  26166  cxpval  26653  lgamgulmlem4  27020  lgamgulmlem5  27021  musumsum  27180  muinv  27181  lgsval  27289  gausslemma2dlem1a  27353  gausslemma2dlem2  27355  gausslemma2dlem3  27356  gausslemma2dlem4  27357  abssval  28256  expsval  28442  vtxval  29094  iedgval  29095  crctcshwlkn0lem2  29904  crctcshwlkn0lem3  29905  crctcshlem4  29913  crctcsh  29917  clwlkclwwlklem2fv1  30090  eucrct2eupth  30340  ccatws1f1o  33037  psgnfzto1stlem  33188  resvval  33419  esplyfv1  33760  smatrcl  33987  smatlem  33988  madjusmdetlem2  34019  madjusmdet  34022  ballotlemsv  34701  ballotlemsf1o  34705  plymulx0  34738  mrsubcv  35745  mrsubrn  35748  rdgprc0  36026  dfrdg2  36028  ditgeq123dv  36456  cbvditgdavw2  36533  csbrdgg  37698  csbfinxpg  37757  finxpreclem3  37762  poimirlem2  37996  poimirlem23  38017  poimirlem24  38018  poimirlem27  38021  itg2addnclem3  38047  itgaddnclem2  38053  ftc1anclem5  38071  cdleme27b  40867  cdleme29b  40874  cdleme31sn  40879  cdleme31fv  40889  cdleme40v  40968  dihffval  41729  dihfval  41730  dihval  41731  prjspnfv01  43081  prjspner01  43082  prjspner1  43083  aomclem8  43513  mnringvald  44664  icccncfext  46337  dvnxpaek  46392  fourierdlem103  46659  fourierdlem104  46660  ioorrnopn  46755  ioorrnopnxr  46757  hsphoival  47029  sge0hsphoire  47039  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  hoidmvlelem5  47049  hoidifhspval3  47069  hspmbllem2  47077  ovolval4  47101  afv2eq12d  47685