Metamath Proof Explorer


Theorem naim1

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

Ref Expression
Assertion naim1 φ ψ ψ χ φ χ

Proof

Step Hyp Ref Expression
1 con3 φ ψ ¬ ψ ¬ φ
2 1 orim1d φ ψ ¬ ψ ¬ χ ¬ φ ¬ χ
3 pm3.13 ¬ ψ χ ¬ ψ ¬ χ
4 pm3.14 ¬ φ ¬ χ ¬ φ χ
5 3 4 imim12i ¬ ψ ¬ χ ¬ φ ¬ χ ¬ ψ χ ¬ φ χ
6 df-nan ψ χ ¬ ψ χ
7 df-nan φ χ ¬ φ χ
8 5 6 7 3imtr4g ¬ ψ ¬ χ ¬ φ ¬ χ ψ χ φ χ
9 2 8 syl φ ψ ψ χ φ χ