Theorem intnanrd 489

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 482	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	nsyl 140	1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

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

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 207  df-an 396

This theorem is referenced by:  bianfd  534  3bior1fand  1478  pr1eqbg  4857  iresn0n0  6072  fvmptopabOLD  7488  frxp2  8169  frxp3  8176  wemappo  9589  axrepnd  10634  axunnd  10636  fzpreddisj  13613  sadadd2lem2  16487  smumullem  16529  nndvdslegcd  16542  divgcdnn  16552  sqgcd  16599  coprm  16748  isnmnd  18751  nfimdetndef  22595  mdetfval1  22596  ibladdlem  25855  lgsval2lem  27351  lgsval4a  27363  lgsdilem  27368  2sqcoprm  27479  addsqn2reurex2  27489  nosepdmlem  27728  nodenselem8  27736  nosupbnd2lem1  27760  nbgrnself  29376  wwlks  29855  iswspthsnon  29876  clwwlknon1nloop  30118  clwwlknon1le1  30120  nfrgr2v  30291  hashxpe  32811  acycgr0v  35153  prclisacycgr  35156  fmlasucdisj  35404  dfrdg4  35952  finxpreclem3  37394  finxpreclem5  37396  ibladdnclem  37683  dihatlat  41336  xppss12  42268  jm2.23  43008  rexanuz2nf  45503  ltnelicc  45510  limciccioolb  45636  dvmptfprodlem  45959  stoweidlem26  46041  fourierdlem12  46134  fourierdlem42  46164  divgcdoddALTV  47669