Theorem ifbieq12d 4518

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ifcif 4489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-un 3918  df-if 4490

This theorem is referenced by:  csbif  4547  csbopg  4857  tz7.44-2  8390  tz7.44-3  8391  boxcutc  8935  unxpdomlem1  9212  ttrcltr  9681  updjudhcoinlf  9914  updjudhcoinrg  9915  dfac12lem1  10123  dfac12r  10126  fin23lem12  10311  fin23lem33  10325  ttukeylem3  10491  ttukey2g  10496  xaddval  13245  seqf1olem2  14074  expval  14095  ccatfval  14606  ccatval1  14610  ccatval2  14611  ccatalpha  14627  relexpsucnnr  15058  ruclem1  16283  eucalgval2  16635  setsstruct  17232  ressval  17289  gsumvalx  18730  gsumpropd  18732  gsumpropd2lem  18733  gsumress  18736  mulgval  19133  pmtrfv  19518  xrsdsval  21526  mvrfval  22095  selvfval  22235  selvvvval  22258  marrepeval  22685  marepveval  22690  mdetunilem9  22742  madutpos  22764  madugsum  22765  minmar1eval  22771  symgmatr01lem  22775  symgmatr01  22776  gsummatr01lem3  22779  gsummatr01lem4  22780  gsummatr01  22781  ptcmplem3  24176  xrhmeo  25070  phtpycc  25115  pcovalg  25136  pcocn  25141  pcohtpylem  25143  pcoass  25148  pcorevlem  25150  ovolunlem1a  25620  ovolunlem1  25621  ioombl1  25686  mbfmax  25773  mbfpos  25775  mbfi1fseqlem2  25840  mbfi1fseq  25845  ditgeq1  25972  ditgeq2  25973  ig1pval  26298  plyn0mulidp  26407  cxpval  26791  lgamgulmlem4  27158  lgamgulmlem5  27159  musumsum  27318  muinv  27319  lgsval  27427  gausslemma2dlem1a  27491  gausslemma2dlem2  27493  gausslemma2dlem3  27494  gausslemma2dlem4  27495  abssval  28394  expsval  28580  vtxval  29287  iedgval  29288  crctcshwlkn0lem2  30097  crctcshwlkn0lem3  30098  crctcshlem4  30106  crctcsh  30110  clwlkclwwlklem2fv1  30283  eucrct2eupth  30533  ccatws1f1o  33208  psgnfzto1stlem  33357  resvval  33588  esplyfv1  33900  smatrcl  34127  smatlem  34128  madjusmdetlem2  34159  madjusmdet  34162  ballotlemsv  34841  ballotlemsf1o  34845  mrsubcv  35897  mrsubrn  35900  rdgprc0  36178  dfrdg2  36180  ditgeq123dv  36618  cbvditgdavw2  36695  csbrdgg  37858  csbfinxpg  37917  finxpreclem3  37922  poimirlem2  38156  poimirlem23  38177  poimirlem24  38178  poimirlem27  38181  itg2addnclem3  38207  itgaddnclem2  38213  ftc1anclem5  38231  cdleme27b  41027  cdleme29b  41034  cdleme31sn  41039  cdleme31fv  41049  cdleme40v  41128  dihffval  41889  dihfval  41890  dihval  41891  prjspnfv01  43243  prjspner01  43244  prjspner1  43245  aomclem8  43675  mnringvald  44824  icccncfext  46488  dvnxpaek  46543  fourierdlem103  46810  fourierdlem104  46811  ioorrnopn  46906  ioorrnopnxr  46908  hsphoival  47180  sge0hsphoire  47190  hoidmvlelem1  47196  hoidmvlelem2  47197  hoidmvlelem3  47198  hoidmvlelem4  47199  hoidmvlelem5  47200  hoidifhspval3  47220  hspmbllem2  47228  ovolval4  47252  afv2eq12d  47836