Theorem intnanrd 937

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 631	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 617  ax-in2 618

This theorem is referenced by:  dcand  938  bianfd  954  3bior1fand  1387  frecabcl  6551  frecsuclem  6558  xrrebnd  10027  fzpreddisj  10279  iseqf1olemqk  10741  gcdsupex  12494  gcdsupcl  12495  nndvdslegcd  12502  divgcdnn  12512  sqgcd  12566  coprm  12682  pclemdc  12827  1arith  12906  ctiunctlemudc  13024  gsum0g  13445  gsumval2  13446  lgsval2lem  15705  lgsval4a  15717  lgsdilem  15722