naim2

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

		Ref	Expression
	Assertion	naim2	$⊢ (φ \to ψ) \to ((χ ⊼ ψ) \to (χ ⊼ φ))$

Step	Hyp	Ref	Expression
1		con3	$⊢ (φ \to ψ) \to (\neg ψ \to \neg φ)$
2	1	orim2d	$⊢ (φ \to ψ) \to ((\neg χ \lor \neg ψ) \to (\neg χ \lor \neg φ))$
3		pm3.13	$⊢ \neg (χ \land ψ) \to (\neg χ \lor \neg ψ)$
4		pm3.14	$⊢ (\neg χ \lor \neg φ) \to \neg (χ \land φ)$
5	3 4	imim12i	$⊢ ((\neg χ \lor \neg ψ) \to (\neg χ \lor \neg φ)) \to (\neg (χ \land ψ) \to \neg (χ \land φ))$
6		df-nan	$⊢ (χ ⊼ ψ) \leftrightarrow \neg (χ \land ψ)$
7		df-nan	$⊢ (χ ⊼ φ) \leftrightarrow \neg (χ \land φ)$
8	5 6 7	3imtr4g	$⊢ ((\neg χ \lor \neg ψ) \to (\neg χ \lor \neg φ)) \to ((χ ⊼ ψ) \to (χ ⊼ φ))$
9	2 8	syl	$⊢ (φ \to ψ) \to ((χ ⊼ ψ) \to (χ ⊼ φ))$

Metamath Proof Explorer