Theorem ifbieq1d 4490

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ifcif 4467

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-un 3941  df-if 4468

This theorem is referenced by:  opeq1  4803  opeq2  4804  oieq1  8976  oieq2  8977  cantnflem1d  9151  cantnflem1  9152  iunfictbso  9540  ttukey2g  9938  bcval  13665  swrdval  14005  summolem2a  15072  zsum  15075  fsum  15077  sumss  15081  sumss2  15083  fsumcvg2  15084  fsumser  15087  isumless  15200  cbvprod  15269  prodmolem2a  15288  zprod  15291  fprod  15295  fprodntriv  15296  prodss  15301  rpnnen2lem1  15567  sadadd2lem  15808  sadadd2  15809  pcmpt  16228  pcmptdvds  16230  prmreclem2  16253  prmreclem4  16255  prmreclem5  16256  prmreclem6  16257  prmrec  16258  ramub1lem2  16363  ramcl  16365  prmop1  16374  prmonn2  16375  prmdvdsprmo  16378  fvprmselelfz  16380  fvprmselgcd1  16381  prmodvdslcmf  16383  prmgapprmo  16398  smndex2dlinvh  18082  pmtrval  18579  pmtrdifellem3  18606  cyggenod2  19004  gsummpt1n0  19085  dmdprdsplitlem  19159  cycsubggenodd  19231  evlslem2  20292  coe1tmmul2fv  20446  coe1pwmulfv  20448  cyggic  20719  dmatmulcl  21109  scmatscmiddistr  21117  marrepval  21171  maducoeval  21248  maducoeval2  21249  minmar1val  21257  fclsval  22616  stdbdmetval  23124  stdbdxmet  23125  pcopt2  23627  cmetcaulem  23891  ovolicc2lem3  24120  ovolicc2lem4  24121  ovolicc2lem5  24122  mbfposb  24254  i1fres  24306  i1fposd  24308  mbfi1fseqlem2  24317  mbfi1fseq  24322  mbfi1flimlem  24323  mbfi1flim  24324  itg2splitlem  24349  itg2cnlem1  24362  itg2cn  24364  isibl  24366  isibl2  24367  iblitg  24369  dfitg  24370  cbvitg  24376  itgeq2  24378  itgvallem  24385  iblneg  24403  itgneg  24404  itgss3  24415  itgcn  24443  deg1suble  24701  elply2  24786  dgrsub  24862  aareccl  24915  vmaval  25690  prmorcht  25755  pclogsum  25791  dchrelbasd  25815  dchrptlem2  25841  bposlem5  25864  lgsfval  25878  lgsdir  25908  lgsdilem2  25909  lgsdi  25910  lgsne0  25911  rplogsumlem2  26061  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  ballotlemsval  31766  ballotlemieq  31774  mrsubfval  32755  poimirlem1  34908  poimirlem5  34912  poimirlem6  34913  poimirlem12  34919  poimirlem22  34929  mblfinlem2  34945  itg2addnclem  34958  ftc1anclem5  34986  ftc1anclem6  34987  cdlemk40  38068  dvnprodlem1  42280  fourierdlem86  42526  fourierdlem97  42537  fourierdlem103  42543  fourierdlem104  42544  fourierdlem112  42552  isomennd  42862  hsphoif  42907  hsphoival  42910  sge0hsphoire  42920  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmv1le  42925  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  hoidmvlelem5  42930  hspval  42940  hoidifhspval2  42946  hoidifhspval3  42950  hspmbllem2  42958  afveq12d  43381