Theorem intnanrd 999

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

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

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 197  df-an 383

This theorem is referenced by:  bianfd  1003  3bior1fand  1587  pr1eqbg  4522  fvmptopab  6845  wemappo  8611  axrepnd  9619  axunnd  9621  fzpreddisj  12598  sadadd2lem2  15381  smumullem  15423  nndvdslegcd  15436  divgcdnn  15445  sqgcd  15487  coprm  15631  pythagtriplem19  15746  isnmnd  17507  nfimdetndef  20614  mdetfval1  20615  ibladdlem  23807  lgsval2lem  25254  lgsval4a  25266  lgsdilem  25271  nbgrnself  26479  wwlks  26964  iswspthsnon  26987  clwwlknclwwlkdifsOLD  27130  clwwlknon1nloop  27275  clwwlknon1le1  27277  nfrgr2v  27455  2sqcoprm  29988  nosepdmlem  32171  nodenselem8  32179  nosupbnd2lem1  32199  dfrdg4  32396  finxpreclem3  33568  finxpreclem5  33570  ibladdnclem  33799  dihatlat  37145  xppss12  37778  jm2.23  38090  ltnelicc  40241  limciccioolb  40372  dvmptfprodlem  40678  stoweidlem26  40761  fourierdlem12  40854  fourierdlem42  40884  divgcdoddALTV  42122