Theorem intnand 943

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 637	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 623  ax-in2 624

This theorem is referenced by:  dcand  945  poxp  6462  cauappcvgprlemladdrl  8018  caucvgprlemladdrl  8039  xrrebnd  10204  fzpreddisj  10461  fzp1nel  10494  fprodntrivap  12334  bitsfzo  12705  bitsmod  12706  gcdsupex  12717  gcdsupcl  12718  gcdnncl  12727  gcd2n0cl  12729  qredeu  12858  cncongr2  12865  divnumden  12957  divdenle  12958  phisum  13002  pythagtriplem4  13030  pythagtriplem8  13034  pythagtriplem9  13035  isnsgrp  13704  ivthinclemdisj  15724  lgsneg  16126  umgredgnlp  16376  umgr2edg1  16433  umgr2edgneu  16436