Metamath Proof Explorer


Theorem ifbieq1d

Description: Equivalence/equality deduction for conditional operators. (Contributed by JJ, 25-Sep-2018)

Ref Expression
Hypotheses ifbieq1d.1
|- ( ph -> ( ps <-> ch ) )
ifbieq1d.2
|- ( ph -> A = B )
Assertion ifbieq1d
|- ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )

Proof

Step Hyp Ref Expression
1 ifbieq1d.1
 |-  ( ph -> ( ps <-> ch ) )
2 ifbieq1d.2
 |-  ( ph -> A = B )
3 1 ifbid
 |-  ( ph -> if ( ps , A , C ) = if ( ch , A , C ) )
4 2 ifeq1d
 |-  ( ph -> if ( ch , A , C ) = if ( ch , B , C ) )
5 3 4 eqtrd
 |-  ( ph -> if ( ps , A , C ) = if ( ch , B , C ) )