Theorem ifbieq1d 3558

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 3557	. 2 |- ( ph -> if ( ps , A , C ) = if ( ch , A , C ) )
3		ifbieq1d.2	. . 3 |- ( ph -> A = B )
4	3	ifeq1d 3553	. 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 3536

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 2741  df-un 3135  df-if 3537

This theorem is referenced by:  ctssdclemn0  7111  ctssdc  7114  enumctlemm  7115  iseqf1olemfvp  10499  seq3f1olemqsum  10502  seq3f1oleml  10505  seq3f1o  10506  bcval  10731  sumrbdclem  11387  summodclem3  11390  summodclem2a  11391  summodc  11393  zsumdc  11394  fsum3  11397  isumss  11401  isumss2  11403  fsum3cvg2  11404  fsum3ser  11407  fsumcl2lem  11408  fsumadd  11416  sumsnf  11419  fsummulc2  11458  isumlessdc  11506  cbvprod  11568  prodrbdclem  11581  prodmodclem3  11585  prodmodclem2a  11586  prodmodc  11588  zproddc  11589  fprodseq  11593  fprodntrivap  11594  prodssdc  11599  fprodmul  11601  prodsnf  11602  pcmpt  12343  pcmptdvds  12345  lgsval  14444  lgsfvalg  14445  lgsdir  14475  lgsdilem2  14476  lgsdi  14477  lgsne0  14478