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  4817  iresn0n0  6014  frxp2  8100  frxp3  8107  wemappo  9478  axrepnd  10523  axunnd  10525  fzpreddisj  13510  sadadd2lem2  16396  smumullem  16438  nndvdslegcd  16451  divgcdnn  16461  sqgcd  16508  coprm  16657  isnmnd  18641  nfimdetndef  22452  mdetfval1  22453  ibladdlem  25697  lgsval2lem  27194  lgsval4a  27206  lgsdilem  27211  2sqcoprm  27322  addsqn2reurex2  27332  nosepdmlem  27571  nodenselem8  27579  nosupbnd2lem1  27603  nbgrnself  29262  wwlks  29738  iswspthsnon  29759  clwwlknon1nloop  30001  clwwlknon1le1  30003  nfrgr2v  30174  tpssad  32441  hashxpe  32705  acycgr0v  35108  prclisacycgr  35111  fmlasucdisj  35359  dfrdg4  35912  finxpreclem3  37354  finxpreclem5  37356  ibladdnclem  37643  dihatlat  41301  xppss12  42190  jm2.23  42958  rexanuz2nf  45461  ltnelicc  45468  limciccioolb  45592  dvmptfprodlem  45915  stoweidlem26  45997  fourierdlem12  46090  fourierdlem42  46120  divgcdoddALTV  47656