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  6384  cauappcvgprlemladdrl  7852  caucvgprlemladdrl  7873  xrrebnd  10023  fzpreddisj  10275  fzp1nel  10308  fprodntrivap  12103  bitsfzo  12474  bitsmod  12475  gcdsupex  12486  gcdsupcl  12487  gcdnncl  12496  gcd2n0cl  12498  qredeu  12627  cncongr2  12634  divnumden  12726  divdenle  12727  phisum  12771  pythagtriplem4  12799  pythagtriplem8  12803  pythagtriplem9  12804  isnsgrp  13447  ivthinclemdisj  15322  lgsneg  15711  umgredgnlp  15958  umgr2edg1  16015  umgr2edgneu  16018