Theorem intnanrd 490

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

Hypothesis

Ref	Expression
intnand.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
intnanrd	⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

Proof of Theorem intnanrd

Step	Hyp	Ref	Expression
1		intnand.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		simpl 483	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	nsyl 140	1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  bianfd  535  3bior1fand  1475  pr1eqbg  4788  iresn0n0  5966  fvmptopabOLD  7339  wemappo  9317  axrepnd  10359  axunnd  10361  fzpreddisj  13314  sadadd2lem2  16166  smumullem  16208  nndvdslegcd  16221  divgcdnn  16231  sqgcd  16279  coprm  16425  isnmnd  18398  nfimdetndef  21747  mdetfval1  21748  ibladdlem  24993  lgsval2lem  26464  lgsval4a  26476  lgsdilem  26481  2sqcoprm  26592  addsqn2reurex2  26602  nbgrnself  27735  wwlks  28209  iswspthsnon  28230  clwwlknon1nloop  28472  clwwlknon1le1  28474  nfrgr2v  28645  hashxpe  31136  acycgr0v  33119  prclisacycgr  33122  fmlasucdisj  33370  frxp2  33800  frxp3  33806  nosepdmlem  33895  nodenselem8  33903  nosupbnd2lem1  33927  dfrdg4  34262  finxpreclem3  35573  finxpreclem5  35575  ibladdnclem  35842  dihatlat  39355  xppss12  40211  jm2.23  40825  ltnelicc  43042  limciccioolb  43169  dvmptfprodlem  43492  stoweidlem26  43574  fourierdlem12  43667  fourierdlem42  43697  divgcdoddALTV  45145