Theorem ifbieq12d 4517

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-un 3919  df-if 4489

This theorem is referenced by:  csbif  4546  csbopg  4855  tz7.44-2  8375  tz7.44-3  8376  boxcutc  8914  unxpdomlem1  9197  ttrcltr  9669  updjudhcoinlf  9885  updjudhcoinrg  9886  dfac12lem1  10097  dfac12r  10100  fin23lem12  10284  fin23lem33  10298  ttukeylem3  10464  ttukey2g  10469  xaddval  13183  seqf1olem2  14007  expval  14028  ccatfval  14538  ccatval1  14542  ccatval2  14543  ccatalpha  14558  relexpsucnnr  14991  ruclem1  16199  eucalgval2  16551  setsstruct  17146  ressval  17203  gsumvalx  18603  gsumpropd  18605  gsumpropd2lem  18606  gsumress  18609  mulgval  19003  pmtrfv  19382  xrsdsval  21327  mvrfval  21890  selvfval  22021  marrepeval  22450  marepveval  22455  mdetunilem9  22507  madutpos  22529  madugsum  22530  minmar1eval  22536  symgmatr01lem  22540  symgmatr01  22541  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  ptcmplem3  23941  xrhmeo  24844  phtpycc  24890  pcovalg  24912  pcocn  24917  pcohtpylem  24919  pcoass  24924  pcorevlem  24926  ovolunlem1a  25397  ovolunlem1  25398  ioombl1  25463  mbfmax  25550  mbfpos  25552  mbfi1fseqlem2  25617  mbfi1fseq  25622  ditgeq1  25749  ditgeq2  25750  ig1pval  26081  cxpval  26573  lgamgulmlem4  26942  lgamgulmlem5  26943  musumsum  27102  muinv  27103  lgsval  27212  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem3  27279  gausslemma2dlem4  27280  abssval  28141  expsval  28311  vtxval  28927  iedgval  28928  crctcshwlkn0lem2  29741  crctcshwlkn0lem3  29742  crctcshlem4  29750  crctcsh  29754  clwlkclwwlklem2fv1  29924  eucrct2eupth  30174  ccatws1f1o  32873  psgnfzto1stlem  33057  resvval  33301  smatrcl  33786  smatlem  33787  madjusmdetlem2  33818  madjusmdet  33821  ballotlemsv  34501  ballotlemsf1o  34505  plymulx0  34538  mrsubcv  35497  mrsubrn  35500  rdgprc0  35781  dfrdg2  35783  ditgeq123dv  36209  cbvditgdavw2  36286  csbrdgg  37317  csbfinxpg  37376  finxpreclem3  37381  poimirlem2  37616  poimirlem23  37637  poimirlem24  37638  poimirlem27  37641  itg2addnclem3  37667  itgaddnclem2  37673  ftc1anclem5  37691  cdleme27b  40362  cdleme29b  40369  cdleme31sn  40374  cdleme31fv  40384  cdleme40v  40463  dihffval  41224  dihfval  41225  dihval  41226  selvvvval  42573  prjspnfv01  42612  prjspner01  42613  prjspner1  42614  aomclem8  43050  mnringvald  44202  icccncfext  45885  dvnxpaek  45940  fourierdlem103  46207  fourierdlem104  46208  ioorrnopn  46303  ioorrnopnxr  46305  hsphoival  46577  sge0hsphoire  46587  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoidmvlelem5  46597  hoidifhspval3  46617  hspmbllem2  46625  ovolval4  46649  afv2eq12d  47216