Theorem naim1

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

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

Proof

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