Theorem intnanrd 493

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  bianfd  542  3bior1fand  1496  pr1eqbg  4812  iresn0n0  6039  frxp2  8118  frxp3  8125  wemappo  9491  axrepnd  10546  axunnd  10548  fzpreddisj  13572  sadadd2lem2  16475  smumullem  16517  nndvdslegcd  16530  divgcdnn  16540  sqgcd  16587  coprm  16737  isnmnd  18763  nfimdetndef  22637  mdetfval1  22638  ibladdlem  25870  lgsval2lem  27359  lgsval4a  27371  lgsdilem  27376  2sqcoprm  27487  addsqn2reurex2  27497  nosepdmlem  27735  nodenselem8  27743  nosupbnd2lem1  27767  pw2cut2  28543  nbgrnself  29517  wwlks  29992  iswspthsnon  30013  clwwlknon1nloop  30258  clwwlknon1le1  30260  nfrgr2v  30431  tpssad  32698  hashxpe  32970  esplyind  33833  acycgr0v  35459  prclisacycgr  35462  fmlasucdisj  35710  dfrdg4  36262  nmulprop  36501  finxpreclem3  37848  finxpreclem5  37850  ibladdnclem  38136  dihatlat  41919  xppss12  42809  jm2.23  43534  rexanuz2nf  46027  ltnelicc  46034  limciccioolb  46158  dvmptfprodlem  46479  stoweidlem26  46561  fourierdlem12  46654  fourierdlem42  46684  divgcdoddALTV  48265