Theorem ifbieq1d 4507

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

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

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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-if 4483

This theorem is used by:  opeq1  4833  opeq2  4834  oieq1  9491  oieq2  9492  cantnflem1d  9674  cantnflem1  9675  ttrcltr  9702  iunfictbso  10142  ttukey2g  10543  bcval  14393  swrdval  14736  summolem2a  15826  zsum  15829  fsum  15831  sumss  15835  sumss2  15837  fsumcvg2  15838  fsumser  15841  isumless  15959  cbvprod  16027  cbvprodv  16028  prodmolem2a  16046  zprod  16049  fprod  16053  fprodntriv  16054  prodss  16059  rpnnen2lem1  16327  sadadd2lem  16574  sadadd2  16575  pcmpt  17009  pcmptdvds  17011  prmreclem2  17034  prmreclem4  17036  prmreclem5  17037  prmreclem6  17038  prmrec  17039  ramub1lem2  17144  ramcl  17146  prmop1  17155  prmonn2  17156  prmdvdsprmo  17159  fvprmselelfz  17161  fvprmselgcd1  17162  prmodvdslcmf  17164  prmgapprmo  17179  smndex2dlinvh  19055  pmtrval  19604  pmtrdifellem3  19631  cyggenod2  20038  gsummpt1n0  20118  dmdprdsplitlem  20192  cycsubggenodd  20264  cyggic  21817  evlslem2  22327  coe1tmmul2fv  22536  coe1pwmulfv  22538  dmatmulcl  22754  scmatscmiddistr  22762  marrepval  22816  maducoeval  22893  maducoeval2  22894  minmar1val  22902  fclsval  24266  stdbdmetval  24772  stdbdxmet  24773  pcopt2  25283  cmetcaulem  25548  ovolicc2lem3  25779  ovolicc2lem4  25780  ovolicc2lem5  25781  mbfposb  25913  i1fres  25965  i1fposd  25967  mbfi1fseqlem2  25976  mbfi1fseq  25981  mbfi1flimlem  25982  mbfi1flim  25983  itg2splitlem  26008  itg2cnlem1  26021  itg2cn  26023  isibl  26025  isibl2  26026  iblitg  26028  dfitg  26029  cbvitg  26035  itgeq2  26037  itgvallem  26044  iblneg  26062  itgneg  26063  itgss3  26074  itgcn  26104  deg1suble  26364  elply2  26453  dgrsub  26530  aareccl  26594  vmaval  27381  prmorcht  27446  pclogsum  27483  dchrelbasd  27507  dchrptlem2  27533  bposlem5  27556  lgsfval  27570  lgsdir  27600  lgsdilem2  27601  lgsdi  27602  lgsne0  27603  rplogsumlem2  27753  pntrlog2bndlem4  27848  pntrlog2bndlem5  27849  elrspunsn  33890  gsummoncoe1fzo  34040  selvply1rhmlem2  34064  extvfval  34075  extvfvv  34077  fldextrspunlsp  34217  extdgfialglem2  34236  ballotlemsval  35053  ballotlemieq  35061  mrsubfval  36170  cbvprodvw2  36934  cbvproddavw  36967  cbvsumdavw2  36982  cbvproddavw2  36983  poimirlem1  38435  poimirlem5  38439  poimirlem6  38440  poimirlem12  38446  poimirlem22  38456  mblfinlem2  38472  itg2addnclem  38485  ftc1anclem5  38511  ftc1anclem6  38512  cdlemk40  41855  fsuppind  43501  cantnfub  44227  dvnprodlem1  46839  fourierdlem86  47085  fourierdlem97  47096  fourierdlem103  47102  fourierdlem104  47103  fourierdlem112  47111  isomennd  47424  hsphoif  47469  hsphoival  47472  sge0hsphoire  47482  hoidmv1lelem2  47485  hoidmv1lelem3  47486  hoidmv1le  47487  hoidmvlelem1  47488  hoidmvlelem2  47489  hoidmvlelem3  47490  hoidmvlelem4  47491  hoidmvlelem5  47492  hspval  47502  hoidifhspval2  47508  hoidifhspval3  47512  hspmbllem2  47520  afveq12d  48086  discsubc  50055  oppfvalg  50117