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  1476  pr1eqbg  4856  iresn0n0  6051  fvmptopabOLD  7460  frxp2  8126  frxp3  8133  wemappo  9540  axrepnd  10585  axunnd  10587  fzpreddisj  13546  sadadd2lem2  16387  smumullem  16429  nndvdslegcd  16442  divgcdnn  16452  sqgcd  16498  coprm  16644  isnmnd  18625  nfimdetndef  22082  mdetfval1  22083  ibladdlem  25328  lgsval2lem  26799  lgsval4a  26811  lgsdilem  26816  2sqcoprm  26927  addsqn2reurex2  26937  nosepdmlem  27175  nodenselem8  27183  nosupbnd2lem1  27207  nbgrnself  28605  wwlks  29078  iswspthsnon  29099  clwwlknon1nloop  29341  clwwlknon1le1  29343  nfrgr2v  29514  hashxpe  32006  acycgr0v  34127  prclisacycgr  34130  fmlasucdisj  34378  dfrdg4  34911  finxpreclem3  36262  finxpreclem5  36264  ibladdnclem  36532  dihatlat  40193  xppss12  41043  jm2.23  41720  rexanuz2nf  44189  ltnelicc  44196  limciccioolb  44323  dvmptfprodlem  44646  stoweidlem26  44728  fourierdlem12  44821  fourierdlem42  44851  divgcdoddALTV  46336