Theorem intnand 932

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Hypothesis

Ref	Expression
intnand.1	|- ( ph -> -. ps )

Assertion

Ref	Expression
intnand	|- ( ph -> -. ( ch /\ ps ) )

Proof of Theorem intnand

Step	Hyp	Ref	Expression
1		intnand.1	. 2 |- ( ph -> -. ps )
2		simpr 110	. 2 |- ( ( ch /\ ps ) -> ps )
3	1, 2	nsyl 629	1 |- ( ph -> -. ( ch /\ ps ) )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-in1 615  ax-in2 616

This theorem is referenced by:  dcand  934  poxp  6285  cauappcvgprlemladdrl  7717  caucvgprlemladdrl  7738  xrrebnd  9885  fzpreddisj  10137  fzp1nel  10170  fprodntrivap  11727  gcdsupex  12094  gcdsupcl  12095  gcdnncl  12104  gcd2n0cl  12106  qredeu  12235  cncongr2  12242  divnumden  12334  divdenle  12335  phisum  12378  pythagtriplem4  12406  pythagtriplem8  12410  pythagtriplem9  12411  isnsgrp  12989  ivthinclemdisj  14794  lgsneg  15140