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  4817  iresn0n0  6046  frxp2  8154  frxp3  8161  wemappo  9536  axrepnd  10672  axunnd  10674  fzpreddisj  13700  sadadd2lem2  16613  smumullem  16655  nndvdslegcd  16668  divgcdnn  16680  sqgcd  16729  coprm  16880  isnmnd  18920  nfimdetndef  22897  mdetfval1  22898  ibladdlem  26133  lgsval2lem  27627  lgsval4a  27639  lgsdilem  27644  2sqcoprm  27755  addsqn2reurex2  27765  nosepdmlem  28033  nodenselem8  28041  nosupbnd2lem1  28065  pw2cut2  28841  nbgrnself  29933  wwlks  30417  iswspthsnon  30438  clwwlknon1nloop  30683  clwwlknon1le1  30685  nfrgr2v  30866  tpssad  33128  hashxpe  33392  esplyind  34200  acycgr0v  35892  prclisacycgr  35895  fmlasucdisj  36143  dfrdg4  36695  nmulprop  36919  finxpreclem3  38296  finxpreclem5  38298  ibladdnclem  38574  dihatlat  42371  xppss12  43263  jm2.23  43982  rexanuz2nf  46471  ltnelicc  46478  limciccioolb  46602  dvmptfprodlem  46923  stoweidlem26  47005  fourierdlem12  47098  fourierdlem42  47128  divgcdoddALTV  48749