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  6442  cauappcvgprlemladdrl  7989  caucvgprlemladdrl  8010  xrrebnd  10175  fzpreddisj  10431  fzp1nel  10464  fprodntrivap  12300  bitsfzo  12671  bitsmod  12672  gcdsupex  12683  gcdsupcl  12684  gcdnncl  12693  gcd2n0cl  12695  qredeu  12824  cncongr2  12831  divnumden  12923  divdenle  12924  phisum  12968  pythagtriplem4  12996  pythagtriplem8  13000  pythagtriplem9  13001  isnsgrp  13674  ivthinclemdisj  15636  lgsneg  16028  umgredgnlp  16278  umgr2edg1  16335  umgr2edgneu  16338