Theorem ifbieq1d 4497

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  ifcif 4473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404  df-v 3443  df-un 3903  df-if 4474

This theorem is referenced by:  opeq1  4817  opeq2  4818  oieq1  9369  oieq2  9370  cantnflem1d  9545  cantnflem1  9546  ttrcltr  9573  iunfictbso  9971  ttukey2g  10373  bcval  14119  swrdval  14454  summolem2a  15526  zsum  15529  fsum  15531  sumss  15535  sumss2  15537  fsumcvg2  15538  fsumser  15541  isumless  15656  cbvprod  15724  prodmolem2a  15743  zprod  15746  fprod  15750  fprodntriv  15751  prodss  15756  rpnnen2lem1  16022  sadadd2lem  16265  sadadd2  16266  pcmpt  16690  pcmptdvds  16692  prmreclem2  16715  prmreclem4  16717  prmreclem5  16718  prmreclem6  16719  prmrec  16720  ramub1lem2  16825  ramcl  16827  prmop1  16836  prmonn2  16837  prmdvdsprmo  16840  fvprmselelfz  16842  fvprmselgcd1  16843  prmodvdslcmf  16845  prmgapprmo  16860  smndex2dlinvh  18652  pmtrval  19155  pmtrdifellem3  19182  cyggenod2  19580  gsummpt1n0  19661  dmdprdsplitlem  19735  cycsubggenodd  19807  cyggic  20886  evlslem2  21395  coe1tmmul2fv  21555  coe1pwmulfv  21557  dmatmulcl  21755  scmatscmiddistr  21763  marrepval  21817  maducoeval  21894  maducoeval2  21895  minmar1val  21903  fclsval  23265  stdbdmetval  23776  stdbdxmet  23777  pcopt2  24292  cmetcaulem  24558  ovolicc2lem3  24789  ovolicc2lem4  24790  ovolicc2lem5  24791  mbfposb  24923  i1fres  24976  i1fposd  24978  mbfi1fseqlem2  24987  mbfi1fseq  24992  mbfi1flimlem  24993  mbfi1flim  24994  itg2splitlem  25019  itg2cnlem1  25032  itg2cn  25034  isibl  25036  isibl2  25037  iblitg  25039  dfitg  25040  cbvitg  25046  itgeq2  25048  itgvallem  25055  iblneg  25073  itgneg  25074  itgss3  25085  itgcn  25115  deg1suble  25378  elply2  25463  dgrsub  25539  aareccl  25592  vmaval  26368  prmorcht  26433  pclogsum  26469  dchrelbasd  26493  dchrptlem2  26519  bposlem5  26542  lgsfval  26556  lgsdir  26586  lgsdilem2  26587  lgsdi  26588  lgsne0  26589  rplogsumlem2  26739  pntrlog2bndlem4  26834  pntrlog2bndlem5  26835  ballotlemsval  32775  ballotlemieq  32783  mrsubfval  33769  poimirlem1  35883  poimirlem5  35887  poimirlem6  35888  poimirlem12  35894  poimirlem22  35904  mblfinlem2  35920  itg2addnclem  35933  ftc1anclem5  35959  ftc1anclem6  35960  cdlemk40  39185  fsuppind  40539  dvnprodlem1  43823  fourierdlem86  44069  fourierdlem97  44080  fourierdlem103  44086  fourierdlem104  44087  fourierdlem112  44095  isomennd  44406  hsphoif  44451  hsphoival  44454  sge0hsphoire  44464  hoidmv1lelem2  44467  hoidmv1lelem3  44468  hoidmv1le  44469  hoidmvlelem1  44470  hoidmvlelem2  44471  hoidmvlelem3  44472  hoidmvlelem4  44473  hoidmvlelem5  44474  hspval  44484  hoidifhspval2  44490  hoidifhspval3  44494  hspmbllem2  44502  afveq12d  44976