Theorem intnand 921

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

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

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

This theorem is referenced by:  dcan  923  poxp  6200  cauappcvgprlemladdrl  7598  caucvgprlemladdrl  7619  xrrebnd  9755  fzpreddisj  10006  fzp1nel  10039  fprodntrivap  11525  gcdsupex  11890  gcdsupcl  11891  gcdnncl  11900  gcd2n0cl  11902  qredeu  12029  cncongr2  12036  divnumden  12128  divdenle  12129  phisum  12172  pythagtriplem4  12200  pythagtriplem8  12204  pythagtriplem9  12205  ivthinclemdisj  13258  lgsneg  13565