Theorem intnand 926

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 623	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 609  ax-in2 610

This theorem is referenced by:  dcan  928  poxp  6211  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  xrrebnd  9776  fzpreddisj  10027  fzp1nel  10060  fprodntrivap  11547  gcdsupex  11912  gcdsupcl  11913  gcdnncl  11922  gcd2n0cl  11924  qredeu  12051  cncongr2  12058  divnumden  12150  divdenle  12151  phisum  12194  pythagtriplem4  12222  pythagtriplem8  12226  pythagtriplem9  12227  isnsgrp  12647  ivthinclemdisj  13412  lgsneg  13719