Theorem ifbieq1d 3592

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1372   ifcif 3570

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rab 2492  df-v 2773  df-un 3169  df-if 3571

This theorem is referenced by:  ctssdclemn0  7211  ctssdc  7214  enumctlemm  7215  iseqf1olemfvp  10653  seq3f1olemqsum  10656  seq3f1oleml  10659  seq3f1o  10660  bcval  10892  sumrbdclem  11659  summodclem3  11662  summodclem2a  11663  summodc  11665  zsumdc  11666  fsum3  11669  isumss  11673  isumss2  11675  fsum3cvg2  11676  fsum3ser  11679  fsumcl2lem  11680  fsumadd  11688  sumsnf  11691  fsummulc2  11730  isumlessdc  11778  cbvprod  11840  prodrbdclem  11853  prodmodclem3  11857  prodmodclem2a  11858  prodmodc  11860  zproddc  11861  fprodseq  11865  fprodntrivap  11866  prodssdc  11871  fprodmul  11873  prodsnf  11874  pcmpt  12637  pcmptdvds  12639  elply2  15178  lgsval  15452  lgsfvalg  15453  lgsdir  15483  lgsdilem2  15484  lgsdi  15485  lgsne0  15486