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  6472  cauappcvgprlemladdrl  8031  caucvgprlemladdrl  8052  xrrebnd  10239  fzpreddisj  10496  fzp1nel  10529  fprodntrivap  12377  bitsfzo  12748  bitsmod  12749  gcdsupex  12760  gcdsupcl  12761  gcdnncl  12770  gcd2n0cl  12772  qredeu  12901  cncongr2  12908  divnumden  13002  divdenle  13003  phisum  13049  pythagtriplem4  13077  pythagtriplem8  13081  pythagtriplem9  13082  isnsgrp  13781  ivthinclemdisj  15878  lgsneg  16360  umgredgnlp  16610  umgr2edg1  16667  umgr2edgneu  16670