Theorem intnand 962

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 477	. 2 |- ( ( ch /\ ps ) -> ps )
3	1, 2	nsyl 135	1 |- ( ph -> -. ( ch /\ ps ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  csbxp  5200  poxp  7289  suppss2  7329  supp0cosupp0  7334  imacosupp  7335  cdadom1  9008  cfsuc  9079  axunnd  9418  difreicc  12304  fzpreddisj  12390  fzp1nel  12424  repsundef  13518  cshnz  13538  fprodntriv  14672  bitsfzo  15157  bitsmod  15158  gcdnncl  15229  gcd2n0cl  15231  qredeu  15372  cncongr2  15382  divnumden  15456  divdenle  15457  phisum  15495  pythagtriplem4  15524  pythagtriplem8  15528  pythagtriplem9  15529  isnsgrp  17288  isnmnd  17298  mgm2nsgrplem2  17406  0ringnnzr  19269  frlmssuvc2  20134  mamufacex  20195  mavmulsolcl  20357  maducoeval2  20446  opnfbas  21646  lgsneg  25046  numedglnl  26039  umgredgnlp  26042  umgr2edg1  26103  umgr2edgneu  26106  uhgrnbgr0nb  26250  nfrgr2v  27136  4cycl2vnunb  27154  numclwwlkffin0  27215  numclwwlk3lem  27241  divnumden2  29564  poseq  31750  nodenselem8  31841  unbdqndv1  32499  relowlssretop  33211  relowlpssretop  33212  finxpreclem6  33233  itg2addnclem2  33462  elpadd0  35095  dihatlat  36623  dihjatcclem1  36707  rmspecnonsq  37472  rpnnen3lem  37598  gtnelicc  39722  xrgtnelicc  39765  limcrecl  39861  sumnnodd  39862  jumpncnp  40111  stoweidlem39  40256  stoweidlem59  40276  fourierdlem12  40336  preimagelt  40912  preimalegt  40913  pgrpgt2nabl  42147  lindslinindsimp1  42246  lmod1zrnlvec  42283