Theorem intnanrd 944

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 637	1 |- ( ph -> -. ( ps /\ ch ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This theorem is used by:  dcand  945  bianfd  961  3bior1fand  1394  frecabcl  6674  frecsuclem  6681  xrrebnd  10238  fzpreddisj  10495  iseqf1olemqk  10965  gcdsupex  12759  gcdsupcl  12760  nndvdslegcd  12767  divgcdnn  12777  sqgcd  12831  coprm  12948  pclemdc  13096  1arith  13175  ctiunctlemudc  13386  gzsum0  13772  gzsumval2  13773  lgsval2lem  16334  lgsval4a  16346  lgsdilem  16351  trlsegvdegfi  16913  idjudju  17252