Theorem intnand 939

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 633	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 619  ax-in2 620

This theorem is referenced by:  dcand  941  poxp  6427  cauappcvgprlemladdrl  7971  caucvgprlemladdrl  7992  xrrebnd  10151  fzpreddisj  10404  fzp1nel  10437  fprodntrivap  12266  bitsfzo  12637  bitsmod  12638  gcdsupex  12649  gcdsupcl  12650  gcdnncl  12659  gcd2n0cl  12661  qredeu  12790  cncongr2  12797  divnumden  12889  divdenle  12890  phisum  12934  pythagtriplem4  12962  pythagtriplem8  12966  pythagtriplem9  12967  isnsgrp  13611  ivthinclemdisj  15497  lgsneg  15889  umgredgnlp  16139  umgr2edg1  16196  umgr2edgneu  16199