Theorem intnand 943

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 637	1 |- ( ph -> -. ( ch /\ ps ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-in1 623  ax-in2 624

This theorem is used by:  dcand  945  poxp  6468  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  xrrebnd  10232  fzpreddisj  10489  fzp1nel  10522  fprodntrivap  12369  bitsfzo  12740  bitsmod  12741  gcdsupex  12752  gcdsupcl  12753  gcdnncl  12762  gcd2n0cl  12764  qredeu  12893  cncongr2  12900  divnumden  12994  divdenle  12995  phisum  13041  pythagtriplem4  13069  pythagtriplem8  13073  pythagtriplem9  13074  isnsgrp  13772  ivthinclemdisj  15793  lgsneg  16265  umgredgnlp  16515  umgr2edg1  16572  umgr2edgneu  16575