Theorem intnanrd 934

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  935  bianfd  951  3bior1fand  1365  frecabcl  6487  frecsuclem  6494  xrrebnd  9943  fzpreddisj  10195  iseqf1olemqk  10654  gcdsupex  12311  gcdsupcl  12312  nndvdslegcd  12319  divgcdnn  12329  sqgcd  12383  coprm  12499  pclemdc  12644  1arith  12723  ctiunctlemudc  12841  gsum0g  13261  gsumval2  13262  lgsval2lem  15520  lgsval4a  15532  lgsdilem  15537