Theorem intnanrd 491

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

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

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 398

This theorem is referenced by:  bianfd  536  3bior1fand  1477  pr1eqbg  4858  iresn0n0  6054  fvmptopabOLD  7464  frxp2  8130  frxp3  8137  wemappo  9544  axrepnd  10589  axunnd  10591  fzpreddisj  13550  sadadd2lem2  16391  smumullem  16433  nndvdslegcd  16446  divgcdnn  16456  sqgcd  16502  coprm  16648  isnmnd  18629  nfimdetndef  22091  mdetfval1  22092  ibladdlem  25337  lgsval2lem  26810  lgsval4a  26822  lgsdilem  26827  2sqcoprm  26938  addsqn2reurex2  26948  nosepdmlem  27186  nodenselem8  27194  nosupbnd2lem1  27218  nbgrnself  28616  wwlks  29089  iswspthsnon  29110  clwwlknon1nloop  29352  clwwlknon1le1  29354  nfrgr2v  29525  hashxpe  32019  acycgr0v  34139  prclisacycgr  34142  fmlasucdisj  34390  dfrdg4  34923  finxpreclem3  36274  finxpreclem5  36276  ibladdnclem  36544  dihatlat  40205  xppss12  41047  jm2.23  41735  rexanuz2nf  44203  ltnelicc  44210  limciccioolb  44337  dvmptfprodlem  44660  stoweidlem26  44742  fourierdlem12  44835  fourierdlem42  44865  divgcdoddALTV  46350