Theorem ifbieq1d 3945

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1381   ifcif 3922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-rab 2800  df-v 3095  df-un 3463  df-if 3923

This theorem is referenced by:  opeq1  4198  opeq2  4199  oieq1  7935  oieq2  7936  cantnflem1d  8105  cantnflem1  8106  cantnflem1dOLD  8128  cantnflem1OLD  8129  iunfictbso  8493  ttukey2g  8894  bcval  12356  swrdval  12618  summolem2a  13511  zsum  13514  fsum  13516  sumss  13520  sumss2  13522  fsumcvg2  13523  fsumser  13526  isumless  13631  rpnnen2lem1  13820  rpnnen  13832  sadadd2lem  13981  sadadd2  13982  pcmpt  14283  pcmptdvds  14285  prmreclem2  14307  prmreclem4  14309  prmreclem5  14310  prmreclem6  14311  prmrec  14312  ramub1lem2  14417  ramcl  14419  pmtrval  16345  pmtrdifellem3  16372  cyggenod2  16757  gsummpt1n0  16861  dmdprdsplitlem  16952  dmdprdsplitlemOLD  16953  evlslem2  18048  coe1tmmul2fv  18187  coe1pwmulfv  18189  cyggic  18478  dmatmulcl  18869  scmatscmiddistr  18877  marrepval  18931  maducoeval  19008  maducoeval2  19009  minmar1val  19017  fclsval  20375  stdbdmetval  20883  stdbdxmet  20884  pcopt2  21389  cmetcaulem  21593  ovolicc2lem3  21796  ovolicc2lem4  21797  ovolicc2lem5  21798  mbfposb  21926  i1fres  21978  i1fposd  21980  mbfi1fseqlem2  21989  mbfi1fseq  21994  mbfi1flimlem  21995  mbfi1flim  21996  itg2splitlem  22021  itg2cnlem1  22034  itg2cn  22036  isibl  22038  isibl2  22039  iblitg  22041  dfitg  22042  cbvitg  22048  itgeq2  22050  itgvallem  22057  iblneg  22075  itgneg  22076  itgss3  22087  itgcn  22115  deg1suble  22374  elply2  22459  dgrsub  22534  aareccl  22587  vmaval  23252  prmorcht  23317  pclogsum  23355  dchrelbasd  23379  dchrptlem2  23405  bposlem5  23428  lgsfval  23441  lgsdir  23470  lgsdilem2  23471  lgsdi  23472  lgsne0  23473  rplogsumlem2  23535  pntrlog2bndlem4  23630  pntrlog2bndlem5  23631  ballotlemsval  28313  ballotlemieq  28321  mrsubfval  28734  cbvprod  29015  prodmolem2a  29034  zprod  29037  fprod  29041  fprodntriv  29042  prodss  29047  mblfinlem2  30020  itg2addnclem  30034  ftc1anclem5  30062  ftc1anclem6  30063  fourierdlem86  31860  fourierdlem97  31871  fourierdlem103  31877  fourierdlem104  31878  fourierdlem112  31886  afveq12d  32052  cdlemk40  36345