Theorem ifbieq1d 4506

Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.)

Hypotheses

Ref	Expression
ifbieq1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
ifbieq1d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifbieq1d	⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Proof of Theorem ifbieq1d

Step	Hyp	Ref	Expression
1		ifbieq1d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	ifbid 4505	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3		ifbieq1d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq1d 4501	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
5	2, 4	eqtrd 2795	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 4151  df-if 4482

This theorem is used by:  opeq1  4832  opeq2  4833  oieq1  9506  oieq2  9507  cantnflem1d  9689  cantnflem1  9690  ttrcltr  9717  iunfictbso  10193  ttukey2g  10594  bcval  14448  swrdval  14791  summolem2a  15881  zsum  15884  fsum  15886  sumss  15890  sumss2  15892  fsumcvg2  15893  fsumser  15896  isumless  16014  cbvprod  16082  cbvprodv  16083  prodmolem2a  16101  zprod  16104  fprod  16108  fprodntriv  16109  prodss  16114  rpnnen2lem1  16382  sadadd2lem  16629  sadadd2  16630  pcmpt  17070  pcmptdvds  17072  prmreclem2  17095  prmreclem4  17097  prmreclem5  17098  prmreclem6  17099  prmrec  17100  ramub1lem2  17205  ramcl  17207  prmop1  17216  prmonn2  17217  prmdvdsprmo  17220  fvprmselelfz  17222  fvprmselgcd1  17223  prmodvdslcmf  17225  prmgapprmo  17240  smndex2dlinvh  19116  pmtrval  19665  pmtrdifellem3  19692  cyggenod2  20099  gsummpt1n0  20179  dmdprdsplitlem  20253  cycsubggenodd  20325  cyggic  21878  evlslem2  22388  coe1tmmul2fv  22597  coe1pwmulfv  22599  dmatmulcl  22815  scmatscmiddistr  22823  marrepval  22877  maducoeval  22954  maducoeval2  22955  minmar1val  22963  fclsval  24327  stdbdmetval  24833  stdbdxmet  24834  pcopt2  25344  cmetcaulem  25609  ovolicc2lem3  25840  ovolicc2lem4  25841  ovolicc2lem5  25842  mbfposb  25974  i1fres  26026  i1fposd  26028  mbfi1fseqlem2  26037  mbfi1fseq  26042  mbfi1flimlem  26043  mbfi1flim  26044  itg2splitlem  26069  itg2cnlem1  26082  itg2cn  26084  isibl  26086  isibl2  26087  iblitg  26089  dfitg  26090  cbvitg  26096  itgeq2  26098  itgvallem  26105  iblneg  26123  itgneg  26124  itgss3  26135  itgcn  26165  deg1suble  26425  elply2  26514  dgrsub  26591  aareccl  26653  vmaval  27440  prmorcht  27505  pclogsum  27542  dchrelbasd  27566  dchrptlem2  27592  bposlem5  27615  lgsfval  27629  lgsdir  27659  lgsdilem2  27660  lgsdi  27661  lgsne0  27662  rplogsumlem2  27812  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  elrspunsn  33979  gsummoncoe1fzo  34129  selvply1rhmlem2  34153  extvfval  34164  extvfvv  34166  fldextrspunlsp  34306  extdgfialglem2  34325  ballotlemsval  35141  ballotlemieq  35149  mrsubfval  36273  cbvprodvw2  37036  cbvproddavw  37069  cbvsumdavw2  37084  cbvproddavw2  37085  poimirlem1  38540  poimirlem5  38544  poimirlem6  38545  poimirlem12  38551  poimirlem22  38561  mblfinlem2  38577  itg2addnclem  38590  ftc1anclem5  38616  ftc1anclem6  38617  cdlemk40  41975  fsuppind  43619  cantnfub  44323  dvnprodlem1  46956  fourierdlem86  47202  fourierdlem97  47213  fourierdlem103  47219  fourierdlem104  47220  fourierdlem112  47228  isomennd  47541  hsphoif  47586  hsphoival  47589  sge0hsphoire  47599  hoidmv1lelem2  47602  hoidmv1lelem3  47603  hoidmv1le  47604  hoidmvlelem1  47605  hoidmvlelem2  47606  hoidmvlelem3  47607  hoidmvlelem4  47608  hoidmvlelem5  47609  hspval  47619  hoidifhspval2  47625  hoidifhspval3  47629  hspmbllem2  47637  afveq12d  48203  discsubc  50172  oppfvalg  50234