Theorem intnand 931

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 628	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 614  ax-in2 615

This theorem is referenced by:  dcan  933  poxp  6223  cauappcvgprlemladdrl  7631  caucvgprlemladdrl  7652  xrrebnd  9790  fzpreddisj  10041  fzp1nel  10074  fprodntrivap  11560  gcdsupex  11925  gcdsupcl  11926  gcdnncl  11935  gcd2n0cl  11937  qredeu  12064  cncongr2  12071  divnumden  12163  divdenle  12164  phisum  12207  pythagtriplem4  12235  pythagtriplem8  12239  pythagtriplem9  12240  isnsgrp  12678  ivthinclemdisj  13689  lgsneg  13996