Theorem ifbieq1d 4510

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 4509	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3		ifbieq1d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq1d 4505	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
5	2, 4	eqtrd 2797	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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-un 3907  df-if 4486

This theorem is used by:  opeq1  4836  opeq2  4837  oieq1  9487  oieq2  9488  cantnflem1d  9670  cantnflem1  9671  ttrcltr  9698  iunfictbso  10120  ttukey2g  10521  bcval  14368  swrdval  14711  summolem2a  15801  zsum  15804  fsum  15806  sumss  15810  sumss2  15812  fsumcvg2  15813  fsumser  15816  isumless  15934  cbvprod  16002  cbvprodv  16003  prodmolem2a  16023  zprod  16026  fprod  16030  fprodntriv  16031  prodss  16036  rpnnen2lem1  16304  sadadd2lem  16551  sadadd2  16552  pcmpt  16986  pcmptdvds  16988  prmreclem2  17011  prmreclem4  17013  prmreclem5  17014  prmreclem6  17015  prmrec  17016  ramub1lem2  17121  ramcl  17123  prmop1  17132  prmonn2  17133  prmdvdsprmo  17136  fvprmselelfz  17138  fvprmselgcd1  17139  prmodvdslcmf  17141  prmgapprmo  17156  smndex2dlinvh  19028  pmtrval  19577  pmtrdifellem3  19604  cyggenod2  20011  gsummpt1n0  20091  dmdprdsplitlem  20165  cycsubggenodd  20237  cyggic  21784  evlslem2  22294  coe1tmmul2fv  22503  coe1pwmulfv  22505  dmatmulcl  22721  scmatscmiddistr  22729  marrepval  22783  maducoeval  22860  maducoeval2  22861  minmar1val  22869  fclsval  24233  stdbdmetval  24739  stdbdxmet  24740  pcopt2  25250  cmetcaulem  25515  ovolicc2lem3  25746  ovolicc2lem4  25747  ovolicc2lem5  25748  mbfposb  25880  i1fres  25932  i1fposd  25934  mbfi1fseqlem2  25943  mbfi1fseq  25948  mbfi1flimlem  25949  mbfi1flim  25950  itg2splitlem  25975  itg2cnlem1  25988  itg2cn  25990  isibl  25992  isibl2  25993  iblitg  25995  dfitg  25996  cbvitg  26003  itgeq2  26005  itgvallem  26012  iblneg  26030  itgneg  26031  itgss3  26042  itgcn  26072  deg1suble  26332  elply2  26421  dgrsub  26497  aareccl  26557  vmaval  27345  prmorcht  27410  pclogsum  27447  dchrelbasd  27471  dchrptlem2  27497  bposlem5  27520  lgsfval  27534  lgsdir  27564  lgsdilem2  27565  lgsdi  27566  lgsne0  27567  rplogsumlem2  27717  pntrlog2bndlem4  27812  pntrlog2bndlem5  27813  elrspunsn  33842  gsummoncoe1fzo  33992  selvply1rhmlem2  34016  extvfval  34027  extvfvv  34029  fldextrspunlsp  34169  extdgfialglem2  34188  ballotlemsval  35005  ballotlemieq  35013  mrsubfval  36072  cbvprodvw2  36852  cbvproddavw  36885  cbvsumdavw2  36900  cbvproddavw2  36901  poimirlem1  38355  poimirlem5  38359  poimirlem6  38360  poimirlem12  38366  poimirlem22  38376  mblfinlem2  38392  itg2addnclem  38405  ftc1anclem5  38431  ftc1anclem6  38432  cdlemk40  41775  fsuppind  43421  cantnfub  44147  dvnprodlem1  46759  fourierdlem86  47005  fourierdlem97  47016  fourierdlem103  47022  fourierdlem104  47023  fourierdlem112  47031  isomennd  47344  hsphoif  47389  hsphoival  47392  sge0hsphoire  47402  hoidmv1lelem2  47405  hoidmv1lelem3  47406  hoidmv1le  47407  hoidmvlelem1  47408  hoidmvlelem2  47409  hoidmvlelem3  47410  hoidmvlelem4  47411  hoidmvlelem5  47412  hspval  47422  hoidifhspval2  47428  hoidifhspval3  47432  hspmbllem2  47440  afveq12d  48006  discsubc  49975  oppfvalg  50037