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  4811  iresn0n0  6009  frxp2  8084  frxp3  8091  wemappo  9460  axrepnd  10507  axunnd  10509  fzpreddisj  13494  sadadd2lem2  16379  smumullem  16421  nndvdslegcd  16434  divgcdnn  16444  sqgcd  16491  coprm  16640  isnmnd  18630  nfimdetndef  22492  mdetfval1  22493  ibladdlem  25737  lgsval2lem  27234  lgsval4a  27246  lgsdilem  27251  2sqcoprm  27362  addsqn2reurex2  27372  nosepdmlem  27611  nodenselem8  27619  nosupbnd2lem1  27643  nbgrnself  29322  wwlks  29798  iswspthsnon  29819  clwwlknon1nloop  30061  clwwlknon1le1  30063  nfrgr2v  30234  tpssad  32501  hashxpe  32765  acycgr0v  35123  prclisacycgr  35126  fmlasucdisj  35374  dfrdg4  35927  finxpreclem3  37369  finxpreclem5  37371  ibladdnclem  37658  dihatlat  41316  xppss12  42205  jm2.23  42972  rexanuz2nf  45475  ltnelicc  45482  limciccioolb  45606  dvmptfprodlem  45929  stoweidlem26  46011  fourierdlem12  46104  fourierdlem42  46134  divgcdoddALTV  47670