Theorem intnand 921

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 109	. 2 |- ( ( ch /\ ps ) -> ps )
3	1, 2	nsyl 618	1 |- ( ph -> -. ( ch /\ ps ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-in1 604  ax-in2 605

This theorem is referenced by:  dcan  923  poxp  6191  cauappcvgprlemladdrl  7589  caucvgprlemladdrl  7610  xrrebnd  9746  fzpreddisj  9996  fzp1nel  10029  fprodntrivap  11511  gcdsupex  11875  gcdsupcl  11876  gcdnncl  11885  gcd2n0cl  11887  qredeu  12008  cncongr2  12015  divnumden  12105  divdenle  12106  phisum  12149  pythagtriplem4  12177  pythagtriplem8  12181  pythagtriplem9  12182  ivthinclemdisj  13159