Theorem ifbieq1d 4501

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

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

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 3395  df-v 3438  df-un 3908  df-if 4477

This theorem is referenced by:  opeq1  4824  opeq2  4825  oieq1  9404  oieq2  9405  cantnflem1d  9584  cantnflem1  9585  ttrcltr  9612  iunfictbso  10008  ttukey2g  10410  bcval  14211  swrdval  14550  summolem2a  15622  zsum  15625  fsum  15627  sumss  15631  sumss2  15633  fsumcvg2  15634  fsumser  15637  isumless  15752  cbvprod  15820  cbvprodv  15821  prodmolem2a  15841  zprod  15844  fprod  15848  fprodntriv  15849  prodss  15854  rpnnen2lem1  16123  sadadd2lem  16370  sadadd2  16371  pcmpt  16804  pcmptdvds  16806  prmreclem2  16829  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  prmrec  16834  ramub1lem2  16939  ramcl  16941  prmop1  16950  prmonn2  16951  prmdvdsprmo  16954  fvprmselelfz  16956  fvprmselgcd1  16957  prmodvdslcmf  16959  prmgapprmo  16974  smndex2dlinvh  18791  pmtrval  19330  pmtrdifellem3  19357  cyggenod2  19764  gsummpt1n0  19844  dmdprdsplitlem  19918  cycsubggenodd  19990  cyggic  21479  evlslem2  21984  coe1tmmul2fv  22162  coe1pwmulfv  22164  dmatmulcl  22385  scmatscmiddistr  22393  marrepval  22447  maducoeval  22524  maducoeval2  22525  minmar1val  22533  fclsval  23893  stdbdmetval  24400  stdbdxmet  24401  pcopt2  24921  cmetcaulem  25186  ovolicc2lem3  25418  ovolicc2lem4  25419  ovolicc2lem5  25420  mbfposb  25552  i1fres  25604  i1fposd  25606  mbfi1fseqlem2  25615  mbfi1fseq  25620  mbfi1flimlem  25621  mbfi1flim  25622  itg2splitlem  25647  itg2cnlem1  25660  itg2cn  25662  isibl  25664  isibl2  25665  iblitg  25667  dfitg  25668  cbvitg  25675  itgeq2  25677  itgvallem  25684  iblneg  25702  itgneg  25703  itgss3  25714  itgcn  25744  deg1suble  26010  elply2  26099  dgrsub  26176  aareccl  26232  vmaval  27021  prmorcht  27086  pclogsum  27124  dchrelbasd  27148  dchrptlem2  27174  bposlem5  27197  lgsfval  27211  lgsdir  27241  lgsdilem2  27242  lgsdi  27243  lgsne0  27244  rplogsumlem2  27394  pntrlog2bndlem4  27489  pntrlog2bndlem5  27490  elrspunsn  33375  gsummoncoe1fzo  33539  fldextrspunlsp  33657  extdgfialglem2  33676  ballotlemsval  34493  ballotlemieq  34501  mrsubfval  35501  cbvprodvw2  36241  cbvproddavw  36274  cbvsumdavw2  36289  cbvproddavw2  36290  poimirlem1  37621  poimirlem5  37625  poimirlem6  37626  poimirlem12  37632  poimirlem22  37642  mblfinlem2  37658  itg2addnclem  37671  ftc1anclem5  37697  ftc1anclem6  37698  cdlemk40  40916  fsuppind  42583  cantnfub  43314  dvnprodlem1  45947  fourierdlem86  46193  fourierdlem97  46204  fourierdlem103  46210  fourierdlem104  46211  fourierdlem112  46219  isomennd  46532  hsphoif  46577  hsphoival  46580  sge0hsphoire  46590  hoidmv1lelem2  46593  hoidmv1lelem3  46594  hoidmv1le  46595  hoidmvlelem1  46596  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvlelem4  46599  hoidmvlelem5  46600  hspval  46610  hoidifhspval2  46616  hoidifhspval3  46620  hspmbllem2  46628  afveq12d  47137  discsubc  49069  oppfvalg  49131