Theorem ifbieq1d 4059

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-un 3545  df-if 4037

This theorem is referenced by:  opeq1  4340  opeq2  4341  oieq1  8300  oieq2  8301  cantnflem1d  8468  cantnflem1  8469  iunfictbso  8820  ttukey2g  9221  bcval  12953  swrdval  13269  summolem2a  14293  zsum  14296  fsum  14298  sumss  14302  sumss2  14304  fsumcvg2  14305  fsumser  14308  isumless  14416  cbvprod  14484  prodmolem2a  14503  zprod  14506  fprod  14510  fprodntriv  14511  prodss  14516  rpnnen2lem1  14782  sadadd2lem  15019  sadadd2  15020  pcmpt  15434  pcmptdvds  15436  prmreclem2  15459  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  prmrec  15464  ramub1lem2  15569  ramcl  15571  prmop1  15580  prmonn2  15581  prmdvdsprmo  15584  fvprmselelfz  15586  fvprmselgcd1  15587  prmodvdslcmf  15589  prmgapprmo  15604  pmtrval  17694  pmtrdifellem3  17721  cyggenod2  18110  gsummpt1n0  18187  dmdprdsplitlem  18259  evlslem2  19333  coe1tmmul2fv  19469  coe1pwmulfv  19471  cyggic  19740  dmatmulcl  20125  scmatscmiddistr  20133  marrepval  20187  maducoeval  20264  maducoeval2  20265  minmar1val  20273  fclsval  21622  stdbdmetval  22129  stdbdxmet  22130  pcopt2  22631  cmetcaulem  22894  ovolicc2lem3  23094  ovolicc2lem4  23095  ovolicc2lem5  23096  mbfposb  23226  i1fres  23278  i1fposd  23280  mbfi1fseqlem2  23289  mbfi1fseq  23294  mbfi1flimlem  23295  mbfi1flim  23296  itg2splitlem  23321  itg2cnlem1  23334  itg2cn  23336  isibl  23338  isibl2  23339  iblitg  23341  dfitg  23342  cbvitg  23348  itgeq2  23350  itgvallem  23357  iblneg  23375  itgneg  23376  itgss3  23387  itgcn  23415  deg1suble  23671  elply2  23756  dgrsub  23832  aareccl  23885  vmaval  24639  prmorcht  24704  pclogsum  24740  dchrelbasd  24764  dchrptlem2  24790  bposlem5  24813  lgsfval  24827  lgsdir  24857  lgsdilem2  24858  lgsdi  24859  lgsne0  24860  rplogsumlem2  24974  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  ballotlemsval  29897  ballotlemieq  29905  mrsubfval  30659  poimirlem1  32580  poimirlem5  32584  poimirlem6  32585  poimirlem12  32591  poimirlem22  32601  mblfinlem2  32617  itg2addnclem  32631  ftc1anclem5  32659  ftc1anclem6  32660  cdlemk40  35223  dvnprodlem1  38836  fourierdlem86  39085  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  isomennd  39421  hsphoif  39466  hsphoival  39469  sge0hsphoire  39479  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmv1le  39484  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  hoidmvlelem5  39489  hspval  39499  hoidifhspval2  39505  hoidifhspval3  39509  hspmbllem2  39517  afveq12d  39862