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  6389  cauappcvgprlemladdrl  7860  caucvgprlemladdrl  7881  xrrebnd  10032  fzpreddisj  10284  fzp1nel  10317  fprodntrivap  12116  bitsfzo  12487  bitsmod  12488  gcdsupex  12499  gcdsupcl  12500  gcdnncl  12509  gcd2n0cl  12511  qredeu  12640  cncongr2  12647  divnumden  12739  divdenle  12740  phisum  12784  pythagtriplem4  12812  pythagtriplem8  12816  pythagtriplem9  12817  isnsgrp  13460  ivthinclemdisj  15335  lgsneg  15724  umgredgnlp  15971  umgr2edg1  16028  umgr2edgneu  16031