Metamath Proof Explorer

Theorem intnan

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993)

Ref Expression
Hypothesis intnan.1 
|- -. ph
Assertion intnan 
|- -. ( ps /\ ph )

Proof

Step Hyp Ref Expression
1 intnan.1 
 |-  -. ph
2 simpr 
 |-  ( ( ps /\ ph ) -> ph )
3 1 2 mto 
 |-  -. ( ps /\ ph )