Theorem ifbieq12d 4554

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-if 4526

This theorem is referenced by:  csbif  4583  csbopg  4891  tz7.44-2  8447  tz7.44-3  8448  boxcutc  8981  unxpdomlem1  9286  ttrcltr  9756  updjudhcoinlf  9972  updjudhcoinrg  9973  dfac12lem1  10184  dfac12r  10187  fin23lem12  10371  fin23lem33  10385  ttukeylem3  10551  ttukey2g  10556  xaddval  13265  seqf1olem2  14083  expval  14104  ccatfval  14611  ccatval1  14615  ccatval2  14616  ccatalpha  14631  relexpsucnnr  15064  ruclem1  16267  eucalgval2  16618  setsstruct  17213  ressval  17277  gsumvalx  18689  gsumpropd  18691  gsumpropd2lem  18692  gsumress  18695  mulgval  19089  pmtrfv  19470  xrsdsval  21428  mvrfval  22001  selvfval  22138  marrepeval  22569  marepveval  22574  mdetunilem9  22626  madutpos  22648  madugsum  22649  minmar1eval  22655  symgmatr01lem  22659  symgmatr01  22660  gsummatr01lem3  22663  gsummatr01lem4  22664  gsummatr01  22665  ptcmplem3  24062  xrhmeo  24977  phtpycc  25023  pcovalg  25045  pcocn  25050  pcohtpylem  25052  pcoass  25057  pcorevlem  25059  ovolunlem1a  25531  ovolunlem1  25532  ioombl1  25597  mbfmax  25684  mbfpos  25686  mbfi1fseqlem2  25751  mbfi1fseq  25756  ditgeq1  25883  ditgeq2  25884  ig1pval  26215  cxpval  26706  lgamgulmlem4  27075  lgamgulmlem5  27076  musumsum  27235  muinv  27236  lgsval  27345  gausslemma2dlem1a  27409  gausslemma2dlem2  27411  gausslemma2dlem3  27412  gausslemma2dlem4  27413  abssval  28263  expsval  28408  vtxval  29017  iedgval  29018  crctcshwlkn0lem2  29831  crctcshwlkn0lem3  29832  crctcshlem4  29840  crctcsh  29844  clwlkclwwlklem2fv1  30014  eucrct2eupth  30264  ccatws1f1o  32936  psgnfzto1stlem  33120  resvval  33353  smatrcl  33795  smatlem  33796  madjusmdetlem2  33827  madjusmdet  33830  ballotlemsv  34512  ballotlemsf1o  34516  plymulx0  34562  mrsubcv  35515  mrsubrn  35518  rdgprc0  35794  dfrdg2  35796  ditgeq123dv  36222  cbvditgdavw2  36299  csbrdgg  37330  csbfinxpg  37389  finxpreclem3  37394  poimirlem2  37629  poimirlem23  37650  poimirlem24  37651  poimirlem27  37654  itg2addnclem3  37680  itgaddnclem2  37686  ftc1anclem5  37704  cdleme27b  40370  cdleme29b  40377  cdleme31sn  40382  cdleme31fv  40392  cdleme40v  40471  dihffval  41232  dihfval  41233  dihval  41234  metakunt3  42208  metakunt4  42209  metakunt6  42211  metakunt7  42212  metakunt8  42213  metakunt10  42215  metakunt11  42216  metakunt12  42217  metakunt20  42225  metakunt21  42226  metakunt22  42227  metakunt32  42237  selvvvval  42595  prjspnfv01  42634  prjspner01  42635  prjspner1  42636  aomclem8  43073  mnringvald  44227  icccncfext  45902  dvnxpaek  45957  fourierdlem103  46224  fourierdlem104  46225  ioorrnopn  46320  ioorrnopnxr  46322  hsphoival  46594  sge0hsphoire  46604  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hoidmvlelem5  46614  hoidifhspval3  46634  hspmbllem2  46642  ovolval4  46666  afv2eq12d  47227