Metamath Proof Explorer

Theorem intnand

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005)

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

Proof

Step Hyp Ref Expression
1 intnand.1 
 |-  ( ph -> -. ps )
2 simpr 
 |-  ( ( ch /\ ps ) -> ps )
3 1 2 nsyl 
 |-  ( ph -> -. ( ch /\ ps ) )