Metamath Proof Explorer

Theorem brif12

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

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

Proof

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