Metamath Proof Explorer

Theorem brif2

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

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

Proof

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