Metamath Proof Explorer

Theorem ifcomnan

Description: Commute the conditions in two nested conditionals if both conditions are not simultaneously true. (Contributed by SO, 15-Jul-2018)

Ref Expression
Assertion ifcomnan 
|- ( -. ( ph /\ ps ) -> if ( ph , A , if ( ps , B , C ) ) = if ( ps , B , if ( ph , A , C ) ) )

Proof

Step Hyp Ref Expression
1 pm3.13 
 |-  ( -. ( ph /\ ps ) -> ( -. ph \/ -. ps ) )
2 iffalse 
 |-  ( -. ph -> if ( ph , A , if ( ps , B , C ) ) = if ( ps , B , C ) )
3 iffalse 
 |-  ( -. ph -> if ( ph , A , C ) = C )
4 3 ifeq2d 
 |-  ( -. ph -> if ( ps , B , if ( ph , A , C ) ) = if ( ps , B , C ) )
5 2 4 eqtr4d 
 |-  ( -. ph -> if ( ph , A , if ( ps , B , C ) ) = if ( ps , B , if ( ph , A , C ) ) )
6 iffalse 
 |-  ( -. ps -> if ( ps , B , C ) = C )
7 6 ifeq2d 
 |-  ( -. ps -> if ( ph , A , if ( ps , B , C ) ) = if ( ph , A , C ) )
8 iffalse 
 |-  ( -. ps -> if ( ps , B , if ( ph , A , C ) ) = if ( ph , A , C ) )
9 7 8 eqtr4d 
 |-  ( -. ps -> if ( ph , A , if ( ps , B , C ) ) = if ( ps , B , if ( ph , A , C ) ) )
10 5 9 jaoi 
 |-  ( ( -. ph \/ -. ps ) -> if ( ph , A , if ( ps , B , C ) ) = if ( ps , B , if ( ph , A , C ) ) )
11 1 10 syl 
 |-  ( -. ( ph /\ ps ) -> if ( ph , A , if ( ps , B , C ) ) = if ( ps , B , if ( ph , A , C ) ) )