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  4821  iresn0n0  6025  fvmptopabOLD  7444  frxp2  8123  frxp3  8130  wemappo  9502  axrepnd  10547  axunnd  10549  fzpreddisj  13534  sadadd2lem2  16420  smumullem  16462  nndvdslegcd  16475  divgcdnn  16485  sqgcd  16532  coprm  16681  isnmnd  18665  nfimdetndef  22476  mdetfval1  22477  ibladdlem  25721  lgsval2lem  27218  lgsval4a  27230  lgsdilem  27235  2sqcoprm  27346  addsqn2reurex2  27356  nosepdmlem  27595  nodenselem8  27603  nosupbnd2lem1  27627  nbgrnself  29286  wwlks  29765  iswspthsnon  29786  clwwlknon1nloop  30028  clwwlknon1le1  30030  nfrgr2v  30201  tpssad  32468  hashxpe  32732  acycgr0v  35135  prclisacycgr  35138  fmlasucdisj  35386  dfrdg4  35939  finxpreclem3  37381  finxpreclem5  37383  ibladdnclem  37670  dihatlat  41328  xppss12  42217  jm2.23  42985  rexanuz2nf  45488  ltnelicc  45495  limciccioolb  45619  dvmptfprodlem  45942  stoweidlem26  46024  fourierdlem12  46117  fourierdlem42  46147  divgcdoddALTV  47683