Metamath Proof Explorer

Theorem brif1

Description: Move a relation inside and outside the conditional operator. (Contributed by SN, 14-Aug-2024)

Ref Expression
Assertion brif1 
|- ( if ( ph , A , B ) R C <-> if- ( ph , A R C , B R C ) )

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( ph -> if ( ph , A , B ) = A )
2 1 breq1d 
 |-  ( ph -> ( if ( ph , A , B ) R C <-> A R C ) )
3 iffalse 
 |-  ( -. ph -> if ( ph , A , B ) = B )
4 3 breq1d 
 |-  ( -. ph -> ( if ( ph , A , B ) R C <-> B R C ) )
5 2 4 casesifp 
 |-  ( if ( ph , A , B ) R C <-> if- ( ph , A R C , B R C ) )