Theorem intnanrd 922

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 108	. 2 |- ( ( ps /\ ch ) -> ps )
3	1, 2	nsyl 618	1 |- ( ph -> -. ( ps /\ ch ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-in1 604  ax-in2 605

This theorem is referenced by:  dcan  923  bianfd  938  frecabcl  6363  frecsuclem  6370  xrrebnd  9751  fzpreddisj  10002  iseqf1olemqk  10425  gcdsupex  11886  gcdsupcl  11887  nndvdslegcd  11894  divgcdnn  11904  sqgcd  11958  coprm  12072  pclemdc  12216  1arith  12293  ctiunctlemudc  12366  lgsval2lem  13511  lgsval4a  13523  lgsdilem  13528