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  6545  frecsuclem  6552  xrrebnd  10015  fzpreddisj  10267  iseqf1olemqk  10729  gcdsupex  12478  gcdsupcl  12479  nndvdslegcd  12486  divgcdnn  12496  sqgcd  12550  coprm  12666  pclemdc  12811  1arith  12890  ctiunctlemudc  13008  gsum0g  13429  gsumval2  13430  lgsval2lem  15689  lgsval4a  15701  lgsdilem  15706