Theorem intnan 755

Description: Introduction of conjunct inside of a contradiction.

Hypothesis

Ref	Expression
intnan.1	|- -. ph

Assertion

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

Proof of Theorem intnan

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

Syntax hints:  -. wn 2   /\ wa 240

This theorem is referenced by:  axnulALT 3443  axnul 3444  imadif 4493  xrltnr 6716  nltmnf 6722  avril1 10142  helloworld 10144  indifdi 13823  dfon2lem7 13855  TFAid 14107  nandsym1 14246  subsym1 14251  ufilen 15579  padd01 17272

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain