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  4815  iresn0n0  6021  frxp2  8096  frxp3  8103  wemappo  9466  axrepnd  10517  axunnd  10519  fzpreddisj  13501  sadadd2lem2  16389  smumullem  16431  nndvdslegcd  16444  divgcdnn  16454  sqgcd  16501  coprm  16650  isnmnd  18675  nfimdetndef  22545  mdetfval1  22546  ibladdlem  25789  lgsval2lem  27286  lgsval4a  27298  lgsdilem  27303  2sqcoprm  27414  addsqn2reurex2  27424  nosepdmlem  27663  nodenselem8  27671  nosupbnd2lem1  27695  pw2cut2  28470  nbgrnself  29444  wwlks  29920  iswspthsnon  29941  clwwlknon1nloop  30186  clwwlknon1le1  30188  nfrgr2v  30359  tpssad  32625  hashxpe  32897  esplyind  33751  acycgr0v  35361  prclisacycgr  35364  fmlasucdisj  35612  dfrdg4  36164  finxpreclem3  37645  finxpreclem5  37647  ibladdnclem  37924  dihatlat  41707  xppss12  42598  jm2.23  43350  rexanuz2nf  45847  ltnelicc  45854  limciccioolb  45978  dvmptfprodlem  46299  stoweidlem26  46381  fourierdlem12  46474  fourierdlem42  46504  divgcdoddALTV  48039