Theorem ifbieq1d 4492

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-if 4468

This theorem is referenced by:  opeq1  4817  opeq2  4818  oieq1  9420  oieq2  9421  cantnflem1d  9600  cantnflem1  9601  ttrcltr  9628  iunfictbso  10027  ttukey2g  10429  bcval  14257  swrdval  14597  summolem2a  15668  zsum  15671  fsum  15673  sumss  15677  sumss2  15679  fsumcvg2  15680  fsumser  15683  isumless  15801  cbvprod  15869  cbvprodv  15870  prodmolem2a  15890  zprod  15893  fprod  15897  fprodntriv  15898  prodss  15903  rpnnen2lem1  16172  sadadd2lem  16419  sadadd2  16420  pcmpt  16854  pcmptdvds  16856  prmreclem2  16879  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  prmrec  16884  ramub1lem2  16989  ramcl  16991  prmop1  17000  prmonn2  17001  prmdvdsprmo  17004  fvprmselelfz  17006  fvprmselgcd1  17007  prmodvdslcmf  17009  prmgapprmo  17024  smndex2dlinvh  18879  pmtrval  19417  pmtrdifellem3  19444  cyggenod2  19851  gsummpt1n0  19931  dmdprdsplitlem  20005  cycsubggenodd  20077  cyggic  21562  evlslem2  22067  coe1tmmul2fv  22253  coe1pwmulfv  22255  dmatmulcl  22475  scmatscmiddistr  22483  marrepval  22537  maducoeval  22614  maducoeval2  22615  minmar1val  22623  fclsval  23983  stdbdmetval  24489  stdbdxmet  24490  pcopt2  25000  cmetcaulem  25265  ovolicc2lem3  25496  ovolicc2lem4  25497  ovolicc2lem5  25498  mbfposb  25630  i1fres  25682  i1fposd  25684  mbfi1fseqlem2  25693  mbfi1fseq  25698  mbfi1flimlem  25699  mbfi1flim  25700  itg2splitlem  25725  itg2cnlem1  25738  itg2cn  25740  isibl  25742  isibl2  25743  iblitg  25745  dfitg  25746  cbvitg  25753  itgeq2  25755  itgvallem  25762  iblneg  25780  itgneg  25781  itgss3  25792  itgcn  25822  deg1suble  26082  elply2  26171  dgrsub  26247  aareccl  26303  vmaval  27090  prmorcht  27155  pclogsum  27192  dchrelbasd  27216  dchrptlem2  27242  bposlem5  27265  lgsfval  27279  lgsdir  27309  lgsdilem2  27310  lgsdi  27311  lgsne0  27312  rplogsumlem2  27462  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  elrspunsn  33504  gsummoncoe1fzo  33672  extvfval  33691  extvfvv  33693  fldextrspunlsp  33834  extdgfialglem2  33853  ballotlemsval  34669  ballotlemieq  34677  mrsubfval  35706  cbvprodvw2  36445  cbvproddavw  36478  cbvsumdavw2  36493  cbvproddavw2  36494  poimirlem1  37956  poimirlem5  37960  poimirlem6  37961  poimirlem12  37967  poimirlem22  37977  mblfinlem2  37993  itg2addnclem  38006  ftc1anclem5  38032  ftc1anclem6  38033  cdlemk40  41377  fsuppind  43037  cantnfub  43767  dvnprodlem1  46392  fourierdlem86  46638  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  fourierdlem112  46664  isomennd  46977  hsphoif  47022  hsphoival  47025  sge0hsphoire  47035  hoidmv1lelem2  47038  hoidmv1lelem3  47039  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hoidmvlelem5  47045  hspval  47055  hoidifhspval2  47061  hoidifhspval3  47065  hspmbllem2  47073  afveq12d  47593  discsubc  49551  oppfvalg  49613