Theorem ifbieq12d 4514

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-un 4154  df-if 4486

This theorem is used by:  csbif  4543  csbopg  4854  tz7.44-2  8440  tz7.44-3  8441  boxcutc  8994  unxpdomlem1  9272  ttrcltr  9741  updjudhcoinlf  10037  updjudhcoinrg  10038  dfac12lem1  10246  dfac12r  10249  fin23lem12  10433  fin23lem33  10447  ttukeylem3  10613  ttukey2g  10618  xaddval  13377  seqf1olem2  14209  expval  14230  ccatfval  14742  ccatval1  14746  ccatval2  14747  ccatalpha  14764  relexpsucnnr  15204  ruclem1  16425  eucalgval2  16782  setsstruct  17380  ressval  17437  gsumvalx  18891  gsumpropd  18893  gsumpropd2lem  18894  gsumress  18897  mulgval  19307  pmtrfv  19693  xrsdsval  21744  mvrfval  22315  selvfval  22455  selvvvval  22478  marrepeval  22905  marepveval  22910  mdetunilem9  22962  madutpos  22984  madugsum  22985  minmar1eval  22991  symgmatr01lem  22995  symgmatr01  22996  gsummatr01lem3  22999  gsummatr01lem4  23000  gsummatr01  23001  ptcmplem3  24400  xrhmeo  25294  phtpycc  25339  pcovalg  25360  pcocn  25365  pcohtpylem  25367  pcoass  25372  pcorevlem  25374  ovolunlem1a  25844  ovolunlem1  25845  ioombl1  25910  mbfmax  25997  mbfpos  25999  mbfi1fseqlem2  26064  mbfi1fseq  26069  ditgeq1  26195  ditgeq2  26196  ig1pval  26521  plyn0mulidp  26629  cxpval  27019  lgamgulmlem4  27386  lgamgulmlem5  27387  musumsum  27546  muinv  27547  lgsval  27655  gausslemma2dlem1a  27719  gausslemma2dlem2  27721  gausslemma2dlem3  27722  gausslemma2dlem4  27723  abssval  28652  expsval  28838  angmgmval  29421  vtxval  29605  iedgval  29606  crctcshwlkn0lem2  30427  crctcshwlkn0lem3  30428  crctcshlem4  30436  crctcsh  30440  clwlkclwwlklem2fv1  30613  eucrct2eupth  30873  ccatws1f1o  33581  psgnfzto1stlem  33728  resvval  33957  esplyfv1  34268  smatrcl  34495  smatlem  34496  madjusmdetlem2  34527  madjusmdet  34530  ballotlemsv  35209  ballotlemsf1o  35213  soinfdom  35797  mrsubcv  36441  mrsubrn  36444  rdgprc0  36732  dfrdg2  36734  ditgeq123dv  37187  cbvditgdavw2  37264  csbrdgg  38443  csbfinxpg  38502  finxpreclem3  38507  poimirlem2  38731  poimirlem23  38752  poimirlem24  38753  poimirlem27  38756  itg2addnclem3  38782  itgaddnclem2  38788  ftc1anclem5  38806  cdleme27b  41616  cdleme29b  41623  cdleme31sn  41628  cdleme31fv  41638  cdleme40v  41717  dihffval  42478  dihfval  42479  dihval  42480  aomclem8  44254  mnringvald  45401  icccncfext  47100  dvnxpaek  47155  fourierdlem103  47422  fourierdlem104  47423  ioorrnopn  47518  ioorrnopnxr  47520  hsphoival  47792  sge0hsphoire  47802  hoidmvlelem1  47808  hoidmvlelem2  47809  hoidmvlelem3  47810  hoidmvlelem4  47811  hoidmvlelem5  47812  hoidifhspval3  47832  hspmbllem2  47840  ovolval4  47864  afv2eq12d  48488