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  6565  frecsuclem  6572  xrrebnd  10054  fzpreddisj  10306  iseqf1olemqk  10770  gcdsupex  12546  gcdsupcl  12547  nndvdslegcd  12554  divgcdnn  12564  sqgcd  12618  coprm  12734  pclemdc  12879  1arith  12958  ctiunctlemudc  13076  gsum0g  13497  gsumval2  13498  lgsval2lem  15758  lgsval4a  15770  lgsdilem  15775  trlsegvdegfi  16337