Theorem intnanrd 939

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  940  bianfd  956  3bior1fand  1389  frecabcl  6567  frecsuclem  6574  xrrebnd  10056  fzpreddisj  10308  iseqf1olemqk  10772  gcdsupex  12548  gcdsupcl  12549  nndvdslegcd  12556  divgcdnn  12566  sqgcd  12620  coprm  12736  pclemdc  12881  1arith  12960  ctiunctlemudc  13078  gsum0g  13499  gsumval2  13500  lgsval2lem  15765  lgsval4a  15777  lgsdilem  15782  trlsegvdegfi  16344