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  6287  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  xrrebnd  9888  fzpreddisj  10140  fzp1nel  10173  fprodntrivap  11730  gcdsupex  12097  gcdsupcl  12098  gcdnncl  12107  gcd2n0cl  12109  qredeu  12238  cncongr2  12245  divnumden  12337  divdenle  12338  phisum  12381  pythagtriplem4  12409  pythagtriplem8  12413  pythagtriplem9  12414  isnsgrp  12992  ivthinclemdisj  14819  lgsneg  15181