Theorem intnanrd 944

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 637	1 |- ( ph -> -. ( ps /\ ch ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-in1 623  ax-in2 624

This theorem is used by:  dcand  945  bianfd  961  3bior1fand  1394  frecabcl  6670  frecsuclem  6677  xrrebnd  10221  fzpreddisj  10478  iseqf1olemqk  10944  gcdsupex  12734  gcdsupcl  12735  nndvdslegcd  12742  divgcdnn  12752  sqgcd  12806  coprm  12922  pclemdc  13067  1arith  13146  ctiunctlemudc  13328  gzsum0  13713  gzsumval2  13714  lgsval2lem  16129  lgsval4a  16141  lgsdilem  16146  trlsegvdegfi  16708