Metamath Proof Explorer


Theorem intn3an1d

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
|- ( ph -> -. ps )
Assertion intn3an1d
|- ( ph -> -. ( ps /\ ch /\ th ) )

Proof

Step Hyp Ref Expression
1 intn3and.1
 |-  ( ph -> -. ps )
2 simp1
 |-  ( ( ps /\ ch /\ th ) -> ps )
3 1 2 nsyl
 |-  ( ph -> -. ( ps /\ ch /\ th ) )