Metamath Proof Explorer


Theorem intn3an3d

Description: Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Hypothesis intn3and.1 φ ¬ ψ
Assertion intn3an3d φ ¬ χ θ ψ

Proof

Step Hyp Ref Expression
1 intn3and.1 φ ¬ ψ
2 simp3 χ θ ψ ψ
3 1 2 nsyl φ ¬ χ θ ψ