Theorem intnanrd 934

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  935  bianfd  951  3bior1fand  1365  frecabcl  6485  frecsuclem  6492  xrrebnd  9941  fzpreddisj  10193  iseqf1olemqk  10652  gcdsupex  12278  gcdsupcl  12279  nndvdslegcd  12286  divgcdnn  12296  sqgcd  12350  coprm  12466  pclemdc  12611  1arith  12690  ctiunctlemudc  12808  gsum0g  13228  gsumval2  13229  lgsval2lem  15487  lgsval4a  15499  lgsdilem  15504