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 ( ¬ ( 𝜑𝜓 ) → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 pm3.13 ( ¬ ( 𝜑𝜓 ) → ( ¬ 𝜑 ∨ ¬ 𝜓 ) )
2 iffalse ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , 𝐶 ) )
3 iffalse ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐶 ) = 𝐶 )
4 3 ifeq2d ( ¬ 𝜑 → if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , 𝐶 ) )
5 2 4 eqtr4d ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) )
6 iffalse ( ¬ 𝜓 → if ( 𝜓 , 𝐵 , 𝐶 ) = 𝐶 )
7 6 ifeq2d ( ¬ 𝜓 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜑 , 𝐴 , 𝐶 ) )
8 iffalse ( ¬ 𝜓 → if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) = if ( 𝜑 , 𝐴 , 𝐶 ) )
9 7 8 eqtr4d ( ¬ 𝜓 → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) )
10 5 9 jaoi ( ( ¬ 𝜑 ∨ ¬ 𝜓 ) → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) )
11 1 10 syl ( ¬ ( 𝜑𝜓 ) → if ( 𝜑 , 𝐴 , if ( 𝜓 , 𝐵 , 𝐶 ) ) = if ( 𝜓 , 𝐵 , if ( 𝜑 , 𝐴 , 𝐶 ) ) )