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 142	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 208  df-an 397

This theorem is referenced by:  bianfd  535  3bior1fand  1468  pr1eqbg  4700  fvmptopab  7075  wemappo  8866  axrepnd  9869  axunnd  9871  fzpreddisj  12810  sadadd2lem2  15636  smumullem  15678  nndvdslegcd  15691  divgcdnn  15700  sqgcd  15742  coprm  15888  isnmnd  17741  nfimdetndef  20886  mdetfval1  20887  ibladdlem  24107  lgsval2lem  25569  lgsval4a  25581  lgsdilem  25586  2sqcoprm  25697  addsqn2reurex2  25707  nbgrnself  26828  wwlks  27299  iswspthsnon  27320  clwwlknon1nloop  27564  clwwlknon1le1  27566  nfrgr2v  27739  hashxpe  30209  acycgr0v  32005  prclisacycgr  32008  fmlasucdisj  32256  nosepdmlem  32798  nodenselem8  32806  nosupbnd2lem1  32826  dfrdg4  33023  finxpreclem3  34226  finxpreclem5  34228  ibladdnclem  34500  dihatlat  38022  xppss12  38666  jm2.23  39099  ltnelicc  41335  limciccioolb  41465  dvmptfprodlem  41792  stoweidlem26  41875  fourierdlem12  41968  fourierdlem42  41998  divgcdoddALTV  43351