Theorem intnanrd 933

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  934  bianfd  950  frecabcl  6454  frecsuclem  6461  xrrebnd  9888  fzpreddisj  10140  iseqf1olemqk  10581  gcdsupex  12097  gcdsupcl  12098  nndvdslegcd  12105  divgcdnn  12115  sqgcd  12169  coprm  12285  pclemdc  12429  1arith  12508  ctiunctlemudc  12597  gsum0g  12982  gsumval2  12983  lgsval2lem  15167  lgsval4a  15179  lgsdilem  15184