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  6290  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  xrrebnd  9894  fzpreddisj  10146  fzp1nel  10179  fprodntrivap  11749  bitsfzo  12119  gcdsupex  12124  gcdsupcl  12125  gcdnncl  12134  gcd2n0cl  12136  qredeu  12265  cncongr2  12272  divnumden  12364  divdenle  12365  phisum  12409  pythagtriplem4  12437  pythagtriplem8  12441  pythagtriplem9  12442  isnsgrp  13049  ivthinclemdisj  14876  lgsneg  15265