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  6457  frecsuclem  6464  xrrebnd  9894  fzpreddisj  10146  iseqf1olemqk  10599  gcdsupex  12124  gcdsupcl  12125  nndvdslegcd  12132  divgcdnn  12142  sqgcd  12196  coprm  12312  pclemdc  12457  1arith  12536  ctiunctlemudc  12654  gsum0g  13039  gsumval2  13040  lgsval2lem  15251  lgsval4a  15263  lgsdilem  15268