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  1479  pr1eqbg  4800  iresn0n0  6019  frxp2  8094  frxp3  8101  wemappo  9464  axrepnd  10517  axunnd  10519  fzpreddisj  13527  sadadd2lem2  16419  smumullem  16461  nndvdslegcd  16474  divgcdnn  16484  sqgcd  16531  coprm  16681  isnmnd  18706  nfimdetndef  22554  mdetfval1  22555  ibladdlem  25787  lgsval2lem  27270  lgsval4a  27282  lgsdilem  27287  2sqcoprm  27398  addsqn2reurex2  27408  nosepdmlem  27647  nodenselem8  27655  nosupbnd2lem1  27679  pw2cut2  28454  nbgrnself  29428  wwlks  29903  iswspthsnon  29924  clwwlknon1nloop  30169  clwwlknon1le1  30171  nfrgr2v  30342  tpssad  32609  hashxpe  32880  esplyind  33719  acycgr0v  35330  prclisacycgr  35333  fmlasucdisj  35581  dfrdg4  36133  finxpreclem3  37709  finxpreclem5  37711  ibladdnclem  37997  dihatlat  41780  xppss12  42670  jm2.23  43424  rexanuz2nf  45920  ltnelicc  45927  limciccioolb  46051  dvmptfprodlem  46372  stoweidlem26  46454  fourierdlem12  46547  fourierdlem42  46577  divgcdoddALTV  48158