Theorem intnand 936

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 631	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 617  ax-in2 618

This theorem is referenced by:  dcand  938  poxp  6368  cauappcvgprlemladdrl  7832  caucvgprlemladdrl  7853  xrrebnd  10003  fzpreddisj  10255  fzp1nel  10288  fprodntrivap  12081  bitsfzo  12452  bitsmod  12453  gcdsupex  12464  gcdsupcl  12465  gcdnncl  12474  gcd2n0cl  12476  qredeu  12605  cncongr2  12612  divnumden  12704  divdenle  12705  phisum  12749  pythagtriplem4  12777  pythagtriplem8  12781  pythagtriplem9  12782  isnsgrp  13425  ivthinclemdisj  15299  lgsneg  15688  umgredgnlp  15935  umgr2edg1  15992  umgr2edgneu  15995