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