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  4811  iresn0n0  6045  frxp2  8164  frxp3  8171  wemappo  9547  axrepnd  10683  axunnd  10685  fzpreddisj  13711  sadadd2lem2  16626  smumullem  16668  nndvdslegcd  16681  divgcdnn  16693  sqgcd  16742  coprm  16893  isnmnd  18933  nfimdetndef  22910  mdetfval1  22911  ibladdlem  26146  lgsval2lem  27640  lgsval4a  27652  lgsdilem  27657  2sqcoprm  27768  addsqn2reurex2  27778  nosepdmlem  28046  nodenselem8  28054  nosupbnd2lem1  28078  pw2cut2  28854  nbgrnself  29946  wwlks  30430  iswspthsnon  30451  clwwlknon1nloop  30696  clwwlknon1le1  30698  nfrgr2v  30879  tpssad  33183  hashxpe  33446  esplyind  34254  j0ltaleph  35948  acycgr0v  35990  prclisacycgr  35993  fmlasucdisj  36251  dfrdg4  36808  nmulprop  37032  finxpreclem3  38410  finxpreclem5  38412  ibladdnclem  38688  dihatlat  42485  xppss12  43377  jm2.23  44097  rexanuz2nf  46596  ltnelicc  46603  limciccioolb  46727  dvmptfprodlem  47048  stoweidlem26  47130  fourierdlem12  47223  fourierdlem42  47253  divgcdoddALTV  48874  parhomne2  50848