Metamath Proof Explorer

Theorem con3dimp

Description: Variant of con3d with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

Ref Expression
Hypothesis con3dimp.1 
|- ( ph -> ( ps -> ch ) )
Assertion con3dimp 
|- ( ( ph /\ -. ch ) -> -. ps )

Proof

Step Hyp Ref Expression
1 con3dimp.1 
 |-  ( ph -> ( ps -> ch ) )
2 1 con3d 
 |-  ( ph -> ( -. ch -> -. ps ) )
3 2 imp 
 |-  ( ( ph /\ -. ch ) -> -. ps )