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  6406  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  xrrebnd  10097  fzpreddisj  10349  fzp1nel  10382  fprodntrivap  12206  bitsfzo  12577  bitsmod  12578  gcdsupex  12589  gcdsupcl  12590  gcdnncl  12599  gcd2n0cl  12601  qredeu  12730  cncongr2  12737  divnumden  12829  divdenle  12830  phisum  12874  pythagtriplem4  12902  pythagtriplem8  12906  pythagtriplem9  12907  isnsgrp  13550  ivthinclemdisj  15431  lgsneg  15823  umgredgnlp  16073  umgr2edg1  16130  umgr2edgneu  16133