Theorem intnand 936

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 631	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 617  ax-in2 618

This theorem is referenced by:  dcand  938  poxp  6392  cauappcvgprlemladdrl  7870  caucvgprlemladdrl  7891  xrrebnd  10047  fzpreddisj  10299  fzp1nel  10332  fprodntrivap  12138  bitsfzo  12509  bitsmod  12510  gcdsupex  12521  gcdsupcl  12522  gcdnncl  12531  gcd2n0cl  12533  qredeu  12662  cncongr2  12669  divnumden  12761  divdenle  12762  phisum  12806  pythagtriplem4  12834  pythagtriplem8  12838  pythagtriplem9  12839  isnsgrp  13482  ivthinclemdisj  15357  lgsneg  15746  umgredgnlp  15996  umgr2edg1  16053  umgr2edgneu  16056