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  8024  caucvgprlemladdrl  8045  xrrebnd  10223  fzpreddisj  10480  fzp1nel  10513  fprodntrivap  12353  bitsfzo  12724  bitsmod  12725  gcdsupex  12736  gcdsupcl  12737  gcdnncl  12746  gcd2n0cl  12748  qredeu  12877  cncongr2  12884  divnumden  12976  divdenle  12977  phisum  13021  pythagtriplem4  13049  pythagtriplem8  13053  pythagtriplem9  13054  isnsgrp  13723  ivthinclemdisj  15743  lgsneg  16155  umgredgnlp  16405  umgr2edg1  16462  umgr2edgneu  16465