Theorem naim2

Description: Constructor theorem for -/\ . (Contributed by Anthony Hart, 1-Sep-2011)

	Ref	Expression
Assertion	naim2	$$⊢\left(\phi \to \psi \right)\to \left(\left(\chi ⊼\psi \right)\to \left(\chi ⊼\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		con3	$$⊢\left(\phi \to \psi \right)\to \left(\neg \psi \to \neg \phi \right)$$
2	1	orim2d	$$⊢\left(\phi \to \psi \right)\to \left(\left(\neg \chi \vee \neg \psi \right)\to \left(\neg \chi \vee \neg \phi \right)\right)$$
3		pm3.13	$$⊢\neg \left(\chi \wedge \psi \right)\to \left(\neg \chi \vee \neg \psi \right)$$
4		pm3.14	$$⊢\left(\neg \chi \vee \neg \phi \right)\to \neg \left(\chi \wedge \phi \right)$$
5	3 4	imim12i	$$⊢\left(\left(\neg \chi \vee \neg \psi \right)\to \left(\neg \chi \vee \neg \phi \right)\right)\to \left(\neg \left(\chi \wedge \psi \right)\to \neg \left(\chi \wedge \phi \right)\right)$$
6		df-nan	$$⊢\left(\chi ⊼\psi \right)\leftrightarrow \neg \left(\chi \wedge \psi \right)$$
7		df-nan	$$⊢\left(\chi ⊼\phi \right)\leftrightarrow \neg \left(\chi \wedge \phi \right)$$
8	5 6 7	3imtr4g	$$⊢\left(\left(\neg \chi \vee \neg \psi \right)\to \left(\neg \chi \vee \neg \phi \right)\right)\to \left(\left(\chi ⊼\psi \right)\to \left(\chi ⊼\phi \right)\right)$$
9	2 8	syl	$$⊢\left(\phi \to \psi \right)\to \left(\left(\chi ⊼\psi \right)\to \left(\chi ⊼\phi \right)\right)$$