Theorem ifan

Description: Rewrite a conjunction in a conditional as two nested conditionals. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Assertion	ifan	$$⊢if\left(\left(\phi \wedge \psi \right),A,B\right)=if\left(\phi ,if\left(\psi ,A,B\right),B\right)$$

Proof

Step	Hyp	Ref	Expression
1		iftrue	$$⊢\phi \to if\left(\phi ,if\left(\psi ,A,B\right),B\right)=if\left(\psi ,A,B\right)$$
2		ibar	$$⊢\phi \to \left(\psi \leftrightarrow \left(\phi \wedge \psi \right)\right)$$
3	2	ifbid	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\left(\phi \wedge \psi \right),A,B\right)$$
4	1 3	eqtr2d	$$⊢\phi \to if\left(\left(\phi \wedge \psi \right),A,B\right)=if\left(\phi ,if\left(\psi ,A,B\right),B\right)$$
5		simpl	$$⊢\left(\phi \wedge \psi \right)\to \phi$$
6	5	con3i	$$⊢\neg \phi \to \neg \left(\phi \wedge \psi \right)$$
7	6	iffalsed	$$⊢\neg \phi \to if\left(\left(\phi \wedge \psi \right),A,B\right)=B$$
8		iffalse	$$⊢\neg \phi \to if\left(\phi ,if\left(\psi ,A,B\right),B\right)=B$$
9	7 8	eqtr4d	$$⊢\neg \phi \to if\left(\left(\phi \wedge \psi \right),A,B\right)=if\left(\phi ,if\left(\psi ,A,B\right),B\right)$$
10	4 9	pm2.61i	$$⊢if\left(\left(\phi \wedge \psi \right),A,B\right)=if\left(\phi ,if\left(\psi ,A,B\right),B\right)$$