Theorem ifbieq1d 4549

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-un 3950  df-if 4526

This theorem is referenced by:  opeq1  4870  opeq2  4871  oieq1  9530  oieq2  9531  cantnflem1d  9706  cantnflem1  9707  ttrcltr  9734  iunfictbso  10132  ttukey2g  10534  bcval  14290  swrdval  14620  summolem2a  15688  zsum  15691  fsum  15693  sumss  15697  sumss2  15699  fsumcvg2  15700  fsumser  15703  isumless  15818  cbvprod  15886  prodmolem2a  15905  zprod  15908  fprod  15912  fprodntriv  15913  prodss  15918  rpnnen2lem1  16185  sadadd2lem  16428  sadadd2  16429  pcmpt  16855  pcmptdvds  16857  prmreclem2  16880  prmreclem4  16882  prmreclem5  16883  prmreclem6  16884  prmrec  16885  ramub1lem2  16990  ramcl  16992  prmop1  17001  prmonn2  17002  prmdvdsprmo  17005  fvprmselelfz  17007  fvprmselgcd1  17008  prmodvdslcmf  17010  prmgapprmo  17025  smndex2dlinvh  18863  pmtrval  19400  pmtrdifellem3  19427  cyggenod2  19834  gsummpt1n0  19914  dmdprdsplitlem  19988  cycsubggenodd  20060  cyggic  21500  evlslem2  22019  coe1tmmul2fv  22191  coe1pwmulfv  22193  dmatmulcl  22396  scmatscmiddistr  22404  marrepval  22458  maducoeval  22535  maducoeval2  22536  minmar1val  22544  fclsval  23906  stdbdmetval  24417  stdbdxmet  24418  pcopt2  24944  cmetcaulem  25210  ovolicc2lem3  25442  ovolicc2lem4  25443  ovolicc2lem5  25444  mbfposb  25576  i1fres  25629  i1fposd  25631  mbfi1fseqlem2  25640  mbfi1fseq  25645  mbfi1flimlem  25646  mbfi1flim  25647  itg2splitlem  25672  itg2cnlem1  25685  itg2cn  25687  isibl  25689  isibl2  25690  iblitg  25692  dfitg  25693  cbvitg  25699  itgeq2  25701  itgvallem  25708  iblneg  25726  itgneg  25727  itgss3  25738  itgcn  25768  deg1suble  26037  elply2  26124  dgrsub  26201  aareccl  26255  vmaval  27039  prmorcht  27104  pclogsum  27142  dchrelbasd  27166  dchrptlem2  27192  bposlem5  27215  lgsfval  27229  lgsdir  27259  lgsdilem2  27260  lgsdi  27261  lgsne0  27262  rplogsumlem2  27412  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  elrspunsn  33140  gsummoncoe1fzo  33259  ballotlemsval  34123  ballotlemieq  34131  mrsubfval  35113  poimirlem1  37089  poimirlem5  37093  poimirlem6  37094  poimirlem12  37100  poimirlem22  37110  mblfinlem2  37126  itg2addnclem  37139  ftc1anclem5  37165  ftc1anclem6  37166  cdlemk40  40385  fsuppind  41814  cantnfub  42741  dvnprodlem1  45325  fourierdlem86  45571  fourierdlem97  45582  fourierdlem103  45588  fourierdlem104  45589  fourierdlem112  45597  isomennd  45910  hsphoif  45955  hsphoival  45958  sge0hsphoire  45968  hoidmv1lelem2  45971  hoidmv1lelem3  45972  hoidmv1le  45973  hoidmvlelem1  45974  hoidmvlelem2  45975  hoidmvlelem3  45976  hoidmvlelem4  45977  hoidmvlelem5  45978  hspval  45988  hoidifhspval2  45994  hoidifhspval3  45998  hspmbllem2  46006  afveq12d  46504