Theorem ifbieq1d 3663

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

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   ifcif 3638

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823  df-un 3224  df-if 3639

This theorem is used by:  ctssdclemn0  7456  ctssdc  7459  enumctlemm  7460  iseqf1olemfvp  10967  seq3f1olemqsum  10970  seq3f1oleml  10973  seq3f1o  10974  bcval  11208  swrdval  11441  sumrbdclem  12168  summodclem3  12171  summodclem2a  12172  summodc  12174  zsumdc  12175  fsum3  12178  isumss  12182  isumss2  12184  fsum3cvg2  12185  fsum3ser  12188  fsumcl2lem  12189  fsumadd  12197  sumsnf  12200  fsummulc2  12239  isumlessdc  12287  cbvprod  12349  prodrbdclem  12362  prodmodclem3  12366  prodmodclem2a  12367  prodmodc  12369  zproddc  12370  fprodseq  12374  fprodntrivap  12375  prodssdc  12380  fprodmul  12382  prodsnf  12383  pcmpt  13150  pcmptdvds  13152  ballotfilemsval  13309  ballotfilemieq  13317  ballotfi  13339  elply2  15978  prmorcht  16299  bposlem5  16332  lgsval  16345  lgsfvalg  16346  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379