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  10171  fzpreddisj  10427  fzp1nel  10460  fprodntrivap  12295  bitsfzo  12666  bitsmod  12667  gcdsupex  12678  gcdsupcl  12679  gcdnncl  12688  gcd2n0cl  12690  qredeu  12819  cncongr2  12826  divnumden  12918  divdenle  12919  phisum  12963  pythagtriplem4  12991  pythagtriplem8  12995  pythagtriplem9  12996  isnsgrp  13703  ivthinclemdisj  15617  lgsneg  16009  umgredgnlp  16259  umgr2edg1  16316  umgr2edgneu  16319