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  4804  iresn0n0  5998  frxp2  8069  frxp3  8076  wemappo  9430  axrepnd  10480  axunnd  10482  fzpreddisj  13468  sadadd2lem2  16356  smumullem  16398  nndvdslegcd  16411  divgcdnn  16421  sqgcd  16468  coprm  16617  isnmnd  18641  nfimdetndef  22499  mdetfval1  22500  ibladdlem  25743  lgsval2lem  27240  lgsval4a  27252  lgsdilem  27257  2sqcoprm  27368  addsqn2reurex2  27378  nosepdmlem  27617  nodenselem8  27625  nosupbnd2lem1  27649  pw2cut2  28377  nbgrnself  29332  wwlks  29808  iswspthsnon  29829  clwwlknon1nloop  30071  clwwlknon1le1  30073  nfrgr2v  30244  tpssad  32511  hashxpe  32781  acycgr0v  35184  prclisacycgr  35187  fmlasucdisj  35435  dfrdg4  35985  finxpreclem3  37427  finxpreclem5  37429  ibladdnclem  37716  dihatlat  41373  xppss12  42262  jm2.23  43029  rexanuz2nf  45530  ltnelicc  45537  limciccioolb  45661  dvmptfprodlem  45982  stoweidlem26  46064  fourierdlem12  46157  fourierdlem42  46187  divgcdoddALTV  47713