Theorem ifbieq1d 4554

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 4553	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐴, 𝐶))
3		ifbieq1d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	ifeq1d 4549	. 2 ⊢ (𝜑 → if(𝜒, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))
5	2, 4	eqtrd 2765	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜒, 𝐵, 𝐶))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1533  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-un 3949  df-if 4531

This theorem is referenced by:  opeq1  4875  opeq2  4876  oieq1  9537  oieq2  9538  cantnflem1d  9713  cantnflem1  9714  ttrcltr  9741  iunfictbso  10139  ttukey2g  10541  bcval  14299  swrdval  14629  summolem2a  15697  zsum  15700  fsum  15702  sumss  15706  sumss2  15708  fsumcvg2  15709  fsumser  15712  isumless  15827  cbvprod  15895  prodmolem2a  15914  zprod  15917  fprod  15921  fprodntriv  15922  prodss  15927  rpnnen2lem1  16194  sadadd2lem  16437  sadadd2  16438  pcmpt  16864  pcmptdvds  16866  prmreclem2  16889  prmreclem4  16891  prmreclem5  16892  prmreclem6  16893  prmrec  16894  ramub1lem2  16999  ramcl  17001  prmop1  17010  prmonn2  17011  prmdvdsprmo  17014  fvprmselelfz  17016  fvprmselgcd1  17017  prmodvdslcmf  17019  prmgapprmo  17034  smndex2dlinvh  18877  pmtrval  19418  pmtrdifellem3  19445  cyggenod2  19852  gsummpt1n0  19932  dmdprdsplitlem  20006  cycsubggenodd  20078  cyggic  21523  evlslem2  22047  coe1tmmul2fv  22222  coe1pwmulfv  22224  dmatmulcl  22446  scmatscmiddistr  22454  marrepval  22508  maducoeval  22585  maducoeval2  22586  minmar1val  22594  fclsval  23956  stdbdmetval  24467  stdbdxmet  24468  pcopt2  24994  cmetcaulem  25260  ovolicc2lem3  25492  ovolicc2lem4  25493  ovolicc2lem5  25494  mbfposb  25626  i1fres  25679  i1fposd  25681  mbfi1fseqlem2  25690  mbfi1fseq  25695  mbfi1flimlem  25696  mbfi1flim  25697  itg2splitlem  25722  itg2cnlem1  25735  itg2cn  25737  isibl  25739  isibl2  25740  iblitg  25742  dfitg  25743  cbvitg  25749  itgeq2  25751  itgvallem  25758  iblneg  25776  itgneg  25777  itgss3  25788  itgcn  25818  deg1suble  26087  elply2  26175  dgrsub  26252  aareccl  26306  vmaval  27090  prmorcht  27155  pclogsum  27193  dchrelbasd  27217  dchrptlem2  27243  bposlem5  27266  lgsfval  27280  lgsdir  27310  lgsdilem2  27311  lgsdi  27312  lgsne0  27313  rplogsumlem2  27463  pntrlog2bndlem4  27558  pntrlog2bndlem5  27559  elrspunsn  33241  gsummoncoe1fzo  33399  ballotlemsval  34259  ballotlemieq  34267  mrsubfval  35249  poimirlem1  37225  poimirlem5  37229  poimirlem6  37230  poimirlem12  37236  poimirlem22  37246  mblfinlem2  37262  itg2addnclem  37275  ftc1anclem5  37301  ftc1anclem6  37302  cdlemk40  40520  fsuppind  41958  cantnfub  42892  dvnprodlem1  45472  fourierdlem86  45718  fourierdlem97  45729  fourierdlem103  45735  fourierdlem104  45736  fourierdlem112  45744  isomennd  46057  hsphoif  46102  hsphoival  46105  sge0hsphoire  46115  hoidmv1lelem2  46118  hoidmv1lelem3  46119  hoidmv1le  46120  hoidmvlelem1  46121  hoidmvlelem2  46122  hoidmvlelem3  46123  hoidmvlelem4  46124  hoidmvlelem5  46125  hspval  46135  hoidifhspval2  46141  hoidifhspval3  46145  hspmbllem2  46153  afveq12d  46651