# Metamath Proof Explorer

## 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(¬{\psi }\to ¬{\phi }\right)$
2 1 orim2d ${⊢}\left({\phi }\to {\psi }\right)\to \left(\left(¬{\chi }\vee ¬{\psi }\right)\to \left(¬{\chi }\vee ¬{\phi }\right)\right)$
3 pm3.13 ${⊢}¬\left({\chi }\wedge {\psi }\right)\to \left(¬{\chi }\vee ¬{\psi }\right)$
4 pm3.14 ${⊢}\left(¬{\chi }\vee ¬{\phi }\right)\to ¬\left({\chi }\wedge {\phi }\right)$
5 3 4 imim12i ${⊢}\left(\left(¬{\chi }\vee ¬{\psi }\right)\to \left(¬{\chi }\vee ¬{\phi }\right)\right)\to \left(¬\left({\chi }\wedge {\psi }\right)\to ¬\left({\chi }\wedge {\phi }\right)\right)$
6 df-nan ${⊢}\left({\chi }⊼{\psi }\right)↔¬\left({\chi }\wedge {\psi }\right)$
7 df-nan ${⊢}\left({\chi }⊼{\phi }\right)↔¬\left({\chi }\wedge {\phi }\right)$
8 5 6 7 3imtr4g ${⊢}\left(\left(¬{\chi }\vee ¬{\psi }\right)\to \left(¬{\chi }\vee ¬{\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)$