Theorem intnand 933

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 629	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 615  ax-in2 616

This theorem is referenced by:  dcand  935  poxp  6325  cauappcvgprlemladdrl  7777  caucvgprlemladdrl  7798  xrrebnd  9948  fzpreddisj  10200  fzp1nel  10233  fprodntrivap  11939  bitsfzo  12310  bitsmod  12311  gcdsupex  12322  gcdsupcl  12323  gcdnncl  12332  gcd2n0cl  12334  qredeu  12463  cncongr2  12470  divnumden  12562  divdenle  12563  phisum  12607  pythagtriplem4  12635  pythagtriplem8  12639  pythagtriplem9  12640  isnsgrp  13282  ivthinclemdisj  15156  lgsneg  15545