Theorem intnanrd 940

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

Hypothesis

Ref	Expression
intnand.1	|- ( ph -> -. ps )

Assertion

Ref	Expression
intnanrd	|- ( ph -> -. ( ps /\ ch ) )

Proof of Theorem intnanrd

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 619  ax-in2 620

This theorem is referenced by:  dcand  941  bianfd  957  3bior1fand  1390  frecabcl  6630  frecsuclem  6637  xrrebnd  10152  fzpreddisj  10405  iseqf1olemqk  10869  gcdsupex  12653  gcdsupcl  12654  nndvdslegcd  12661  divgcdnn  12671  sqgcd  12725  coprm  12841  pclemdc  12986  1arith  13065  ctiunctlemudc  13188  gsum0g  13609  gsumval2  13610  lgsval2lem  15883  lgsval4a  15895  lgsdilem  15900  trlsegvdegfi  16462