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  6675  frecsuclem  6682  xrrebnd  10237  fzpreddisj  10494  iseqf1olemqk  10964  gcdsupex  12758  gcdsupcl  12759  nndvdslegcd  12766  divgcdnn  12776  sqgcd  12830  coprm  12947  pclemdc  13095  1arith  13174  ctiunctlemudc  13385  gzsum0  13771  gzsumval2  13772  lgsval2lem  16351  lgsval4a  16363  lgsdilem  16368  trlsegvdegfi  16930  idjudju  17269