Theorem ifbieq1d 4109

Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018.)

Hypotheses

Ref	Expression
ifbieq1d.1	|- ( ph -> ( ps <-> ch ) )
ifbieq1d.2	|- ( ph -> A = B )

Assertion

Ref	Expression
ifbieq1d	|- ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )

Proof of Theorem ifbieq1d

Step	Hyp	Ref	Expression
1		ifbieq1d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	ifbid 4108	. 2 |- ( ph -> if ( ps , A , C ) = if ( ch , A , C ) )
3		ifbieq1d.2	. . 3 |- ( ph -> A = B )
4	3	ifeq1d 4104	. 2 |- ( ph -> if ( ch , A , C ) = if ( ch , B , C ) )
5	2, 4	eqtrd 2656	1 |- ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-un 3579  df-if 4087

This theorem is referenced by:  opeq1  4402  opeq2  4403  oieq1  8417  oieq2  8418  cantnflem1d  8585  cantnflem1  8586  iunfictbso  8937  ttukey2g  9338  bcval  13091  swrdval  13417  summolem2a  14446  zsum  14449  fsum  14451  sumss  14455  sumss2  14457  fsumcvg2  14458  fsumser  14461  isumless  14577  cbvprod  14645  prodmolem2a  14664  zprod  14667  fprod  14671  fprodntriv  14672  prodss  14677  rpnnen2lem1  14943  sadadd2lem  15181  sadadd2  15182  pcmpt  15596  pcmptdvds  15598  prmreclem2  15621  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  prmrec  15626  ramub1lem2  15731  ramcl  15733  prmop1  15742  prmonn2  15743  prmdvdsprmo  15746  fvprmselelfz  15748  fvprmselgcd1  15749  prmodvdslcmf  15751  prmgapprmo  15766  pmtrval  17871  pmtrdifellem3  17898  cyggenod2  18287  gsummpt1n0  18364  dmdprdsplitlem  18436  evlslem2  19512  coe1tmmul2fv  19648  coe1pwmulfv  19650  cyggic  19921  dmatmulcl  20306  scmatscmiddistr  20314  marrepval  20368  maducoeval  20445  maducoeval2  20446  minmar1val  20454  fclsval  21812  stdbdmetval  22319  stdbdxmet  22320  pcopt2  22823  cmetcaulem  23086  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2lem5  23289  mbfposb  23420  i1fres  23472  i1fposd  23474  mbfi1fseqlem2  23483  mbfi1fseq  23488  mbfi1flimlem  23489  mbfi1flim  23490  itg2splitlem  23515  itg2cnlem1  23528  itg2cn  23530  isibl  23532  isibl2  23533  iblitg  23535  dfitg  23536  cbvitg  23542  itgeq2  23544  itgvallem  23551  iblneg  23569  itgneg  23570  itgss3  23581  itgcn  23609  deg1suble  23867  elply2  23952  dgrsub  24028  aareccl  24081  vmaval  24839  prmorcht  24904  pclogsum  24940  dchrelbasd  24964  dchrptlem2  24990  bposlem5  25013  lgsfval  25027  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  rplogsumlem2  25174  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  ballotlemsval  30570  ballotlemieq  30578  mrsubfval  31405  poimirlem1  33410  poimirlem5  33414  poimirlem6  33415  poimirlem12  33421  poimirlem22  33431  mblfinlem2  33447  itg2addnclem  33461  ftc1anclem5  33489  ftc1anclem6  33490  cdlemk40  36205  dvnprodlem1  40161  fourierdlem86  40409  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  isomennd  40745  hsphoif  40790  hsphoival  40793  sge0hsphoire  40803  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmv1le  40808  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  hoidmvlelem5  40813  hspval  40823  hoidifhspval2  40829  hoidifhspval3  40833  hspmbllem2  40841  afveq12d  41213