Theorem intnanrd 940

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 633	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 619  ax-in2 620

This theorem is referenced by:  dcand  941  bianfd  957  3bior1fand  1390  frecabcl  6608  frecsuclem  6615  xrrebnd  10115  fzpreddisj  10368  iseqf1olemqk  10832  gcdsupex  12608  gcdsupcl  12609  nndvdslegcd  12616  divgcdnn  12626  sqgcd  12680  coprm  12796  pclemdc  12941  1arith  13020  ctiunctlemudc  13138  gsum0g  13559  gsumval2  13560  lgsval2lem  15829  lgsval4a  15841  lgsdilem  15846  trlsegvdegfi  16408