Theorem ifbieq1d 3877

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 3876	. 2 |- ( ph -> if ( ps , A , C ) = if ( ch , A , C ) )
3		ifbieq1d.2	. . 3 |- ( ph -> A = B )
4	3	ifeq1d 3872	. 2 |- ( ph -> if ( ch , A , C ) = if ( ch , B , C ) )
5	2, 4	eqtrd 2462	1 |- ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   ifcif 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-rab 2723  df-v 3024  df-un 3384  df-if 3855

This theorem is referenced by:  opeq1  4130  opeq2  4131  oieq1  7980  oieq2  7981  cantnflem1d  8145  cantnflem1  8146  iunfictbso  8496  ttukey2g  8897  bcval  12439  swrdval  12719  summolem2a  13724  zsum  13727  fsum  13729  sumss  13733  sumss2  13735  fsumcvg2  13736  fsumser  13739  isumless  13846  cbvprod  13912  prodmolem2a  13931  zprod  13934  fprod  13938  fprodntriv  13939  prodss  13944  rpnnen2lem1  14210  rpnnen  14222  sadadd2lem  14376  sadadd2  14377  pcmpt  14780  pcmptdvds  14782  prmreclem2  14804  prmreclem4  14806  prmreclem5  14807  prmreclem6  14808  prmrec  14809  ramub1lem2  14928  ramcl  14930  prmop1  14939  prmonn2  14940  prmdvdsprmo  14943  fvprmselelfz  14945  fvprmselgcd1  14946  prmodvdslcmf  14948  prmormapnnOLD  14957  prmdvdsprmorOLD  14958  prmorlefacOLD  14961  prmgapprmo  14976  pmtrval  17035  pmtrdifellem3  17062  cyggenod2  17463  gsummpt1n0  17540  dmdprdsplitlem  17613  evlslem2  18678  coe1tmmul2fv  18814  coe1pwmulfv  18816  cyggic  19085  dmatmulcl  19467  scmatscmiddistr  19475  marrepval  19529  maducoeval  19606  maducoeval2  19607  minmar1val  19615  fclsval  20965  stdbdmetval  21471  stdbdxmet  21472  pcopt2  21996  cmetcaulem  22200  ovolicc2lem3  22414  ovolicc2lem4OLD  22415  ovolicc2lem4  22416  ovolicc2lem5  22417  mbfposb  22551  i1fres  22605  i1fposd  22607  mbfi1fseqlem2  22616  mbfi1fseq  22621  mbfi1flimlem  22622  mbfi1flim  22623  itg2splitlem  22648  itg2cnlem1  22661  itg2cn  22663  isibl  22665  isibl2  22666  iblitg  22668  dfitg  22669  cbvitg  22675  itgeq2  22677  itgvallem  22684  iblneg  22702  itgneg  22703  itgss3  22714  itgcn  22742  deg1suble  22998  elply2  23092  dgrsub  23168  aareccl  23224  vmaval  23982  prmorcht  24047  pclogsum  24085  dchrelbasd  24109  dchrptlem2  24135  bposlem5  24158  lgsfval  24171  lgsdir  24200  lgsdilem2  24201  lgsdi  24202  lgsne0  24203  rplogsumlem2  24265  pntrlog2bndlem4  24360  pntrlog2bndlem5  24361  ballotlemsval  29293  ballotlemieq  29301  ballotlemsvalOLD  29331  ballotlemieqOLD  29339  mrsubfval  30098  poimirlem1  31848  poimirlem5  31852  poimirlem6  31853  poimirlem12  31859  poimirlem22  31869  mblfinlem2  31885  itg2addnclem  31900  ftc1anclem5  31928  ftc1anclem6  31929  cdlemk40  34396  dvnprodlem1  37704  fourierdlem86  37939  fourierdlem97  37950  fourierdlem103  37956  fourierdlem104  37957  fourierdlem112  37965  isomennd  38203  hsphoif  38245  hsphoival  38248  sge0hsphoire  38258  hoidmv1lelem2  38261  hoidmv1lelem3  38262  hoidmv1le  38263  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvlelem4  38267  hoidmvlelem5  38268  afveq12d  38448