Theorem ifbieq1d 4248

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1631  ifcif 4225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-un 3728  df-if 4226

This theorem is referenced by:  opeq1  4539  opeq2  4540  oieq1  8573  oieq2  8574  cantnflem1d  8749  cantnflem1  8750  iunfictbso  9137  ttukey2g  9540  bcval  13295  swrdval  13625  summolem2a  14654  zsum  14657  fsum  14659  sumss  14663  sumss2  14665  fsumcvg2  14666  fsumser  14669  isumless  14784  cbvprod  14852  prodmolem2a  14871  zprod  14874  fprod  14878  fprodntriv  14879  prodss  14884  rpnnen2lem1  15149  sadadd2lem  15389  sadadd2  15390  pcmpt  15803  pcmptdvds  15805  prmreclem2  15828  prmreclem4  15830  prmreclem5  15831  prmreclem6  15832  prmrec  15833  ramub1lem2  15938  ramcl  15940  prmop1  15949  prmonn2  15950  prmdvdsprmo  15953  fvprmselelfz  15955  fvprmselgcd1  15956  prmodvdslcmf  15958  prmgapprmo  15973  pmtrval  18078  pmtrdifellem3  18105  cyggenod2  18494  gsummpt1n0  18571  dmdprdsplitlem  18644  evlslem2  19727  coe1tmmul2fv  19863  coe1pwmulfv  19865  cyggic  20136  dmatmulcl  20524  scmatscmiddistr  20532  marrepval  20586  maducoeval  20663  maducoeval2  20664  minmar1val  20672  fclsval  22032  stdbdmetval  22539  stdbdxmet  22540  pcopt2  23042  cmetcaulem  23305  ovolicc2lem3  23507  ovolicc2lem4  23508  ovolicc2lem5  23509  mbfposb  23640  i1fres  23692  i1fposd  23694  mbfi1fseqlem2  23703  mbfi1fseq  23708  mbfi1flimlem  23709  mbfi1flim  23710  itg2splitlem  23735  itg2cnlem1  23748  itg2cn  23750  isibl  23752  isibl2  23753  iblitg  23755  dfitg  23756  cbvitg  23762  itgeq2  23764  itgvallem  23771  iblneg  23789  itgneg  23790  itgss3  23801  itgcn  23829  deg1suble  24087  elply2  24172  dgrsub  24248  aareccl  24301  vmaval  25060  prmorcht  25125  pclogsum  25161  dchrelbasd  25185  dchrptlem2  25211  bposlem5  25234  lgsfval  25248  lgsdir  25278  lgsdilem2  25279  lgsdi  25280  lgsne0  25281  rplogsumlem2  25395  pntrlog2bndlem4  25490  pntrlog2bndlem5  25491  ballotlemsval  30910  ballotlemieq  30918  mrsubfval  31743  poimirlem1  33743  poimirlem5  33747  poimirlem6  33748  poimirlem12  33754  poimirlem22  33764  mblfinlem2  33780  itg2addnclem  33793  ftc1anclem5  33821  ftc1anclem6  33822  cdlemk40  36726  dvnprodlem1  40679  fourierdlem86  40926  fourierdlem97  40937  fourierdlem103  40943  fourierdlem104  40944  fourierdlem112  40952  isomennd  41265  hsphoif  41310  hsphoival  41313  sge0hsphoire  41323  hoidmv1lelem2  41326  hoidmv1lelem3  41327  hoidmv1le  41328  hoidmvlelem1  41329  hoidmvlelem2  41330  hoidmvlelem3  41331  hoidmvlelem4  41332  hoidmvlelem5  41333  hspval  41343  hoidifhspval2  41349  hoidifhspval3  41353  hspmbllem2  41361  afveq12d  41733