Theorem ifbieq1d 3807

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   ifcif 3786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2719  df-v 2969  df-un 3328  df-if 3787

This theorem is referenced by:  opeq1  4054  opeq2  4055  oieq1  7718  oieq2  7719  cantnflem1d  7888  cantnflem1  7889  cantnflem1dOLD  7911  cantnflem1OLD  7912  iunfictbso  8276  ttukey2g  8677  bcval  12072  swrdval  12305  summolem2a  13184  zsum  13187  fsum  13189  sumss  13193  sumss2  13195  fsumcvg2  13196  fsumser  13199  isumless  13300  rpnnen2lem1  13489  rpnnen  13501  sadadd2lem  13647  sadadd2  13648  pcmpt  13946  pcmptdvds  13948  prmreclem2  13970  prmreclem4  13972  prmreclem5  13973  prmreclem6  13974  prmrec  13975  ramub1lem2  14080  ramcl  14082  pmtrdifellem3  15975  cyggenod2  16353  dmdprdsplitlem  16522  dmdprdsplitlemOLD  16523  evlslem2  17572  coe1tmmul2fv  17706  coe1pwmulfv  17708  cyggic  17980  marrepval  18348  minmar1val  18429  fclsval  19556  stdbdmetval  20064  stdbdxmet  20065  pcopt2  20570  cmetcaulem  20774  ovolicc2lem3  20977  ovolicc2lem4  20978  ovolicc2lem5  20979  mbfposb  21106  i1fres  21158  i1fposd  21160  mbfi1fseqlem2  21169  mbfi1fseq  21174  mbfi1flimlem  21175  mbfi1flim  21176  itg2splitlem  21201  itg2cnlem1  21214  itg2cn  21216  isibl  21218  isibl2  21219  iblitg  21221  dfitg  21222  cbvitg  21228  itgeq2  21230  itgvallem  21237  iblneg  21255  itgneg  21256  itgss3  21267  itgcn  21295  deg1suble  21554  elply2  21639  dgrsub  21714  aareccl  21767  vmaval  22426  prmorcht  22491  pclogsum  22529  dchrelbasd  22553  dchrptlem2  22579  bposlem5  22602  lgsfval  22615  lgsdir  22644  lgsdilem2  22645  lgsdi  22646  lgsne0  22647  rplogsumlem2  22709  pntrlog2bndlem4  22804  pntrlog2bndlem5  22805  itg2addnclem  28396  dmatmulcl  30802  scmatmulcl  30809