This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝜑 , 𝐴 , 𝐶 ) ) )