Theorem ifbieq1d 3916

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

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1455   ifcif 3893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-un 3421  df-if 3894

This theorem is referenced by:  opeq1  4180  opeq2  4181  oieq1  8053  oieq2  8054  cantnflem1d  8219  cantnflem1  8220  iunfictbso  8571  ttukey2g  8972  bcval  12521  swrdval  12810  summolem2a  13830  zsum  13833  fsum  13835  sumss  13839  sumss2  13841  fsumcvg2  13842  fsumser  13845  isumless  13952  cbvprod  14018  prodmolem2a  14037  zprod  14040  fprod  14044  fprodntriv  14045  prodss  14050  rpnnen2lem1  14316  rpnnen  14328  sadadd2lem  14482  sadadd2  14483  pcmpt  14886  pcmptdvds  14888  prmreclem2  14910  prmreclem4  14912  prmreclem5  14913  prmreclem6  14914  prmrec  14915  ramub1lem2  15034  ramcl  15036  prmop1  15045  prmonn2  15046  prmdvdsprmo  15049  fvprmselelfz  15051  fvprmselgcd1  15052  prmodvdslcmf  15054  prmormapnnOLD  15063  prmdvdsprmorOLD  15064  prmorlefacOLD  15067  prmgapprmo  15082  pmtrval  17141  pmtrdifellem3  17168  cyggenod2  17569  gsummpt1n0  17646  dmdprdsplitlem  17719  evlslem2  18784  coe1tmmul2fv  18920  coe1pwmulfv  18922  cyggic  19192  dmatmulcl  19574  scmatscmiddistr  19582  marrepval  19636  maducoeval  19713  maducoeval2  19714  minmar1val  19722  fclsval  21072  stdbdmetval  21578  stdbdxmet  21579  pcopt2  22103  cmetcaulem  22307  ovolicc2lem3  22521  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  ovolicc2lem5  22524  mbfposb  22658  i1fres  22712  i1fposd  22714  mbfi1fseqlem2  22723  mbfi1fseq  22728  mbfi1flimlem  22729  mbfi1flim  22730  itg2splitlem  22755  itg2cnlem1  22768  itg2cn  22770  isibl  22772  isibl2  22773  iblitg  22775  dfitg  22776  cbvitg  22782  itgeq2  22784  itgvallem  22791  iblneg  22809  itgneg  22810  itgss3  22821  itgcn  22849  deg1suble  23105  elply2  23199  dgrsub  23275  aareccl  23331  vmaval  24089  prmorcht  24154  pclogsum  24192  dchrelbasd  24216  dchrptlem2  24242  bposlem5  24265  lgsfval  24278  lgsdir  24307  lgsdilem2  24308  lgsdi  24309  lgsne0  24310  rplogsumlem2  24372  pntrlog2bndlem4  24467  pntrlog2bndlem5  24468  ballotlemsval  29390  ballotlemieq  29398  ballotlemsvalOLD  29428  ballotlemieqOLD  29436  mrsubfval  30195  poimirlem1  31986  poimirlem5  31990  poimirlem6  31991  poimirlem12  31997  poimirlem22  32007  mblfinlem2  32023  itg2addnclem  32038  ftc1anclem5  32066  ftc1anclem6  32067  cdlemk40  34529  dvnprodlem1  37859  fourierdlem86  38094  fourierdlem97  38105  fourierdlem103  38111  fourierdlem104  38112  fourierdlem112  38120  isomennd  38390  hsphoif  38436  hsphoival  38439  sge0hsphoire  38449  hoidmv1lelem2  38452  hoidmv1lelem3  38453  hoidmv1le  38454  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem3  38457  hoidmvlelem4  38458  hoidmvlelem5  38459  hspval  38469  hoidifhspval2  38475  hoidifhspval3  38479  hspmbllem2  38487  afveq12d  38673