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

This theorem is referenced by:  bianfd  534  3bior1fand  1472  pr1eqbg  4849  iresn0n0  6043  fvmptopabOLD  7456  frxp2  8124  frxp3  8131  wemappo  9540  axrepnd  10585  axunnd  10587  fzpreddisj  13547  sadadd2lem2  16388  smumullem  16430  nndvdslegcd  16443  divgcdnn  16453  sqgcd  16499  coprm  16645  isnmnd  18661  nfimdetndef  22413  mdetfval1  22414  ibladdlem  25671  lgsval2lem  27156  lgsval4a  27168  lgsdilem  27173  2sqcoprm  27284  addsqn2reurex2  27294  nosepdmlem  27532  nodenselem8  27540  nosupbnd2lem1  27564  nbgrnself  29085  wwlks  29558  iswspthsnon  29579  clwwlknon1nloop  29821  clwwlknon1le1  29823  nfrgr2v  29994  hashxpe  32488  acycgr0v  34628  prclisacycgr  34631  fmlasucdisj  34879  dfrdg4  35418  finxpreclem3  36764  finxpreclem5  36766  ibladdnclem  37034  dihatlat  40695  xppss12  41540  jm2.23  42224  rexanuz2nf  44688  ltnelicc  44695  limciccioolb  44822  dvmptfprodlem  45145  stoweidlem26  45227  fourierdlem12  45320  fourierdlem42  45350  divgcdoddALTV  46835