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  6508  frecsuclem  6515  xrrebnd  9976  fzpreddisj  10228  iseqf1olemqk  10689  gcdsupex  12393  gcdsupcl  12394  nndvdslegcd  12401  divgcdnn  12411  sqgcd  12465  coprm  12581  pclemdc  12726  1arith  12805  ctiunctlemudc  12923  gsum0g  13343  gsumval2  13344  lgsval2lem  15602  lgsval4a  15614  lgsdilem  15619