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 ) )

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 623  ax-in2 624

This theorem is referenced by:  dcand  945  bianfd  961  3bior1fand  1394  frecabcl  6660  frecsuclem  6667  xrrebnd  10200  fzpreddisj  10456  iseqf1olemqk  10922  gcdsupex  12712  gcdsupcl  12713  nndvdslegcd  12720  divgcdnn  12730  sqgcd  12784  coprm  12900  pclemdc  13045  1arith  13124  ctiunctlemudc  13306  gzsum0  13690  gzsumval2  13691  lgsval2lem  16043  lgsval4a  16055  lgsdilem  16060  trlsegvdegfi  16622