Theorem ifbieq1d 3955

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1374   ifcif 3932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-rab 2816  df-v 3108  df-un 3474  df-if 3933

This theorem is referenced by:  opeq1  4206  opeq2  4207  oieq1  7926  oieq2  7927  cantnflem1d  8096  cantnflem1  8097  cantnflem1dOLD  8119  cantnflem1OLD  8120  iunfictbso  8484  ttukey2g  8885  bcval  12337  swrdval  12594  summolem2a  13486  zsum  13489  fsum  13491  sumss  13495  sumss2  13497  fsumcvg2  13498  fsumser  13501  isumless  13609  rpnnen2lem1  13798  rpnnen  13810  sadadd2lem  13957  sadadd2  13958  pcmpt  14259  pcmptdvds  14261  prmreclem2  14283  prmreclem4  14285  prmreclem5  14286  prmreclem6  14287  prmrec  14288  ramub1lem2  14393  ramcl  14395  pmtrdifellem3  16292  cyggenod2  16672  gsummpt1n0  16776  dmdprdsplitlem  16867  dmdprdsplitlemOLD  16868  evlslem2  17944  coe1tmmul2fv  18083  coe1pwmulfv  18085  cyggic  18371  dmatmulcl  18762  scmatscmiddistr  18770  marrepval  18824  minmar1val  18910  fclsval  20237  stdbdmetval  20745  stdbdxmet  20746  pcopt2  21251  cmetcaulem  21455  ovolicc2lem3  21658  ovolicc2lem4  21659  ovolicc2lem5  21660  mbfposb  21788  i1fres  21840  i1fposd  21842  mbfi1fseqlem2  21851  mbfi1fseq  21856  mbfi1flimlem  21857  mbfi1flim  21858  itg2splitlem  21883  itg2cnlem1  21896  itg2cn  21898  isibl  21900  isibl2  21901  iblitg  21903  dfitg  21904  cbvitg  21910  itgeq2  21912  itgvallem  21919  iblneg  21937  itgneg  21938  itgss3  21949  itgcn  21977  deg1suble  22236  elply2  22321  dgrsub  22396  aareccl  22449  vmaval  23108  prmorcht  23173  pclogsum  23211  dchrelbasd  23235  dchrptlem2  23261  bposlem5  23284  lgsfval  23297  lgsdir  23326  lgsdilem2  23327  lgsdi  23328  lgsne0  23329  rplogsumlem2  23391  pntrlog2bndlem4  23486  pntrlog2bndlem5  23487  itg2addnclem  29630