Theorem intnanrd 495

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 488	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
3	1, 2	nsyl 141	1 ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bianfd  544  3bior1fand  1507  pr1eqbg  4824  iresn0n0  6058  frxp2  8142  frxp3  8149  wemappo  9514  axrepnd  10590  axunnd  10592  fzpreddisj  13613  sadadd2lem2  16525  smumullem  16567  nndvdslegcd  16580  divgcdnn  16590  sqgcd  16637  coprm  16787  isnmnd  18817  nfimdetndef  22775  mdetfval1  22776  ibladdlem  26008  lgsval2lem  27500  lgsval4a  27512  lgsdilem  27517  2sqcoprm  27628  addsqn2reurex2  27638  nosepdmlem  27876  nodenselem8  27884  nosupbnd2lem1  27908  pw2cut2  28684  nbgrnself  29738  wwlks  30213  iswspthsnon  30234  clwwlknon1nloop  30479  clwwlknon1le1  30481  nfrgr2v  30652  tpssad  32914  hashxpe  33181  esplyind  33988  acycgr0v  35653  prclisacycgr  35656  fmlasucdisj  35904  dfrdg4  36456  nmulprop  36695  finxpreclem3  38072  finxpreclem5  38074  ibladdnclem  38360  dihatlat  42141  xppss12  43033  jm2.23  43756  rexanuz2nf  46239  ltnelicc  46246  limciccioolb  46370  dvmptfprodlem  46691  stoweidlem26  46773  fourierdlem12  46866  fourierdlem42  46896  divgcdoddALTV  48480