Theorem intnanrd 963

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)

Hypothesis

Ref	Expression
intnand.1	|- ( ph -> -. ps )

Assertion

Ref	Expression
intnanrd	|- ( ph -> -. ( ps /\ ch ) )

Proof of Theorem intnanrd

Step	Hyp	Ref	Expression
1		intnand.1	. 2 |- ( ph -> -. ps )
2		simpl 473	. 2 |- ( ( ps /\ ch ) -> ps )
3	1, 2	nsyl 135	1 |- ( ph -> -. ( ps /\ ch ) )

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:  bianfd  967  3bior1fand  1439  pr1eqbg  4390  fvmptopab  6697  wemappo  8454  axrepnd  9416  axunnd  9418  fzpreddisj  12390  sadadd2lem2  15172  smumullem  15214  nndvdslegcd  15227  divgcdnn  15236  sqgcd  15278  coprm  15423  pythagtriplem19  15538  isnmnd  17298  nfimdetndef  20395  mdetfval1  20396  ibladdlem  23586  lgsval2lem  25032  lgsval4a  25044  lgsdilem  25049  nbgrnself  26257  wwlks  26727  clwwlknclwwlkdifs  26873  nfrgr2v  27136  2sqcoprm  29647  nosepdmlem  31833  nodenselem8  31841  nosupbnd2lem1  31861  dfrdg4  32058  finxpreclem3  33230  finxpreclem5  33232  ibladdnclem  33466  dihatlat  36623  jm2.23  37563  ltnelicc  39719  limciccioolb  39853  dvmptfprodlem  40159  stoweidlem26  40243  fourierdlem12  40336  fourierdlem42  40366  divgcdoddALTV  41593