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  6670  frecsuclem  6677  xrrebnd  10232  fzpreddisj  10489  iseqf1olemqk  10959  gcdsupex  12753  gcdsupcl  12754  nndvdslegcd  12761  divgcdnn  12771  sqgcd  12825  coprm  12942  pclemdc  13090  1arith  13169  ctiunctlemudc  13380  gzsum0  13766  gzsumval2  13767  lgsval2lem  16295  lgsval4a  16307  lgsdilem  16312  trlsegvdegfi  16874