Theorem intnand 938

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  940  poxp  6397  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  xrrebnd  10054  fzpreddisj  10306  fzp1nel  10339  fprodntrivap  12150  bitsfzo  12521  bitsmod  12522  gcdsupex  12533  gcdsupcl  12534  gcdnncl  12543  gcd2n0cl  12545  qredeu  12674  cncongr2  12681  divnumden  12773  divdenle  12774  phisum  12818  pythagtriplem4  12846  pythagtriplem8  12850  pythagtriplem9  12851  isnsgrp  13494  ivthinclemdisj  15370  lgsneg  15759  umgredgnlp  16009  umgr2edg1  16066  umgr2edgneu  16069