Metamath Proof Explorer

Theorem intnanrd

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

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

Proof

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