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	$$⊢\neg \left(\phi \wedge \psi \right)\to if\left(\phi ,A,if\left(\psi ,B,C\right)\right)=if\left(\psi ,B,if\left(\phi ,A,C\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		pm3.13	$$⊢\neg \left(\phi \wedge \psi \right)\to \left(\neg \phi \vee \neg \psi \right)$$
2		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,if\left(\psi ,B,C\right)\right)=if\left(\psi ,B,C\right)$$
3		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,C\right)=C$$
4	3	ifeq2d	$$⊢\neg \phi \to if\left(\psi ,B,if\left(\phi ,A,C\right)\right)=if\left(\psi ,B,C\right)$$
5	2 4	eqtr4d	$$⊢\neg \phi \to if\left(\phi ,A,if\left(\psi ,B,C\right)\right)=if\left(\psi ,B,if\left(\phi ,A,C\right)\right)$$
6		iffalse	$$⊢\neg \psi \to if\left(\psi ,B,C\right)=C$$
7	6	ifeq2d	$$⊢\neg \psi \to if\left(\phi ,A,if\left(\psi ,B,C\right)\right)=if\left(\phi ,A,C\right)$$
8		iffalse	$$⊢\neg \psi \to if\left(\psi ,B,if\left(\phi ,A,C\right)\right)=if\left(\phi ,A,C\right)$$
9	7 8	eqtr4d	$$⊢\neg \psi \to if\left(\phi ,A,if\left(\psi ,B,C\right)\right)=if\left(\psi ,B,if\left(\phi ,A,C\right)\right)$$
10	5 9	jaoi	$$⊢\left(\neg \phi \vee \neg \psi \right)\to if\left(\phi ,A,if\left(\psi ,B,C\right)\right)=if\left(\psi ,B,if\left(\phi ,A,C\right)\right)$$
11	1 10	syl	$$⊢\neg \left(\phi \wedge \psi \right)\to if\left(\phi ,A,if\left(\psi ,B,C\right)\right)=if\left(\psi ,B,if\left(\phi ,A,C\right)\right)$$