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  1474  pr1eqbg  4784  iresn0n0  5952  fvmptopab  7308  wemappo  9238  axrepnd  10281  axunnd  10283  fzpreddisj  13234  sadadd2lem2  16085  smumullem  16127  nndvdslegcd  16140  divgcdnn  16150  sqgcd  16198  coprm  16344  isnmnd  18304  nfimdetndef  21646  mdetfval1  21647  ibladdlem  24889  lgsval2lem  26360  lgsval4a  26372  lgsdilem  26377  2sqcoprm  26488  addsqn2reurex2  26498  nbgrnself  27629  wwlks  28101  iswspthsnon  28122  clwwlknon1nloop  28364  clwwlknon1le1  28366  nfrgr2v  28537  hashxpe  31029  acycgr0v  33010  prclisacycgr  33013  fmlasucdisj  33261  frxp2  33718  frxp3  33724  nosepdmlem  33813  nodenselem8  33821  nosupbnd2lem1  33845  dfrdg4  34180  finxpreclem3  35491  finxpreclem5  35493  ibladdnclem  35760  dihatlat  39275  xppss12  40130  jm2.23  40734  ltnelicc  42925  limciccioolb  43052  dvmptfprodlem  43375  stoweidlem26  43457  fourierdlem12  43550  fourierdlem42  43580  divgcdoddALTV  45022