Theorem ifbieq1d 3570

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1363   ifcif 3548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-rab 2476  df-v 2753  df-un 3147  df-if 3549

This theorem is referenced by:  ctssdclemn0  7126  ctssdc  7129  enumctlemm  7130  iseqf1olemfvp  10514  seq3f1olemqsum  10517  seq3f1oleml  10520  seq3f1o  10521  bcval  10746  sumrbdclem  11402  summodclem3  11405  summodclem2a  11406  summodc  11408  zsumdc  11409  fsum3  11412  isumss  11416  isumss2  11418  fsum3cvg2  11419  fsum3ser  11422  fsumcl2lem  11423  fsumadd  11431  sumsnf  11434  fsummulc2  11473  isumlessdc  11521  cbvprod  11583  prodrbdclem  11596  prodmodclem3  11600  prodmodclem2a  11601  prodmodc  11603  zproddc  11604  fprodseq  11608  fprodntrivap  11609  prodssdc  11614  fprodmul  11616  prodsnf  11617  pcmpt  12358  pcmptdvds  12360  lgsval  14788  lgsfvalg  14789  lgsdir  14819  lgsdilem2  14820  lgsdi  14821  lgsne0  14822