Metamath Proof Explorer

Theorem ifor

Description: Rewrite a disjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Assertion ifor 
|- if ( ( ph \/ ps ) , A , B ) = if ( ph , A , if ( ps , A , B ) )

Proof

Step Hyp Ref Expression
1 iftrue 
 |-  ( ( ph \/ ps ) -> if ( ( ph \/ ps ) , A , B ) = A )
2 1 orcs 
 |-  ( ph -> if ( ( ph \/ ps ) , A , B ) = A )
3 iftrue 
 |-  ( ph -> if ( ph , A , if ( ps , A , B ) ) = A )
4 2 3 eqtr4d 
 |-  ( ph -> if ( ( ph \/ ps ) , A , B ) = if ( ph , A , if ( ps , A , B ) ) )
5 iffalse 
 |-  ( -. ph -> if ( ph , A , if ( ps , A , B ) ) = if ( ps , A , B ) )
6 biorf 
 |-  ( -. ph -> ( ps <-> ( ph \/ ps ) ) )
7 6 ifbid 
 |-  ( -. ph -> if ( ps , A , B ) = if ( ( ph \/ ps ) , A , B ) )
8 5 7 eqtr2d 
 |-  ( -. ph -> if ( ( ph \/ ps ) , A , B ) = if ( ph , A , if ( ps , A , B ) ) )
9 4 8 pm2.61i 
 |-  if ( ( ph \/ ps ) , A , B ) = if ( ph , A , if ( ps , A , B ) )