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  6441  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  xrrebnd  10174  fzpreddisj  10430  fzp1nel  10463  fprodntrivap  12299  bitsfzo  12670  bitsmod  12671  gcdsupex  12682  gcdsupcl  12683  gcdnncl  12692  gcd2n0cl  12694  qredeu  12823  cncongr2  12830  divnumden  12922  divdenle  12923  phisum  12967  pythagtriplem4  12995  pythagtriplem8  12999  pythagtriplem9  13000  isnsgrp  13673  ivthinclemdisj  15635  lgsneg  16027  umgredgnlp  16277  umgr2edg1  16334  umgr2edgneu  16337