Theorem intnanrd 933

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 629	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 615  ax-in2 616

This theorem is referenced by:  dcand  934  bianfd  950  frecabcl  6466  frecsuclem  6473  xrrebnd  9911  fzpreddisj  10163  iseqf1olemqk  10616  gcdsupex  12149  gcdsupcl  12150  nndvdslegcd  12157  divgcdnn  12167  sqgcd  12221  coprm  12337  pclemdc  12482  1arith  12561  ctiunctlemudc  12679  gsum0g  13098  gsumval2  13099  lgsval2lem  15335  lgsval4a  15347  lgsdilem  15352