Theorem ifbieq1d 3921

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1370   ifcif 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-un 3442  df-if 3901

This theorem is referenced by:  opeq1  4168  opeq2  4169  oieq1  7838  oieq2  7839  cantnflem1d  8008  cantnflem1  8009  cantnflem1dOLD  8031  cantnflem1OLD  8032  iunfictbso  8396  ttukey2g  8797  bcval  12198  swrdval  12432  summolem2a  13311  zsum  13314  fsum  13316  sumss  13320  sumss2  13322  fsumcvg2  13323  fsumser  13326  isumless  13427  rpnnen2lem1  13616  rpnnen  13628  sadadd2lem  13774  sadadd2  13775  pcmpt  14073  pcmptdvds  14075  prmreclem2  14097  prmreclem4  14099  prmreclem5  14100  prmreclem6  14101  prmrec  14102  ramub1lem2  14207  ramcl  14209  pmtrdifellem3  16104  cyggenod2  16484  gsummpt1n0  16579  dmdprdsplitlem  16657  dmdprdsplitlemOLD  16658  evlslem2  17722  coe1tmmul2fv  17856  coe1pwmulfv  17858  cyggic  18131  marrepval  18501  minmar1val  18587  fclsval  19714  stdbdmetval  20222  stdbdxmet  20223  pcopt2  20728  cmetcaulem  20932  ovolicc2lem3  21135  ovolicc2lem4  21136  ovolicc2lem5  21137  mbfposb  21265  i1fres  21317  i1fposd  21319  mbfi1fseqlem2  21328  mbfi1fseq  21333  mbfi1flimlem  21334  mbfi1flim  21335  itg2splitlem  21360  itg2cnlem1  21373  itg2cn  21375  isibl  21377  isibl2  21378  iblitg  21380  dfitg  21381  cbvitg  21387  itgeq2  21389  itgvallem  21396  iblneg  21414  itgneg  21415  itgss3  21426  itgcn  21454  deg1suble  21713  elply2  21798  dgrsub  21873  aareccl  21926  vmaval  22585  prmorcht  22650  pclogsum  22688  dchrelbasd  22712  dchrptlem2  22738  bposlem5  22761  lgsfval  22774  lgsdir  22803  lgsdilem2  22804  lgsdi  22805  lgsne0  22806  rplogsumlem2  22868  pntrlog2bndlem4  22963  pntrlog2bndlem5  22964  itg2addnclem  28592  dmatmulcl  31059  scmatmulcl  31066