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  6452  frecsuclem  6459  xrrebnd  9885  fzpreddisj  10137  iseqf1olemqk  10578  gcdsupex  12094  gcdsupcl  12095  nndvdslegcd  12102  divgcdnn  12112  sqgcd  12166  coprm  12282  pclemdc  12426  1arith  12505  ctiunctlemudc  12594  gsum0g  12979  gsumval2  12980  lgsval2lem  15126  lgsval4a  15138  lgsdilem  15143