Theorem ifbieq1d 3557

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   ifcif 3535

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2740  df-un 3134  df-if 3536

This theorem is referenced by:  ctssdclemn0  7109  ctssdc  7112  enumctlemm  7113  iseqf1olemfvp  10497  seq3f1olemqsum  10500  seq3f1oleml  10503  seq3f1o  10504  bcval  10729  sumrbdclem  11385  summodclem3  11388  summodclem2a  11389  summodc  11391  zsumdc  11392  fsum3  11395  isumss  11399  isumss2  11401  fsum3cvg2  11402  fsum3ser  11405  fsumcl2lem  11406  fsumadd  11414  sumsnf  11417  fsummulc2  11456  isumlessdc  11504  cbvprod  11566  prodrbdclem  11579  prodmodclem3  11583  prodmodclem2a  11584  prodmodc  11586  zproddc  11587  fprodseq  11591  fprodntrivap  11592  prodssdc  11597  fprodmul  11599  prodsnf  11600  pcmpt  12341  pcmptdvds  12343  lgsval  14408  lgsfvalg  14409  lgsdir  14439  lgsdilem2  14440  lgsdi  14441  lgsne0  14442