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 142	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 210  df-an 400

This theorem is referenced by:  bianfd  538  3bior1fand  1478  pr1eqbg  4767  iresn0n0  5923  fvmptopab  7266  wemappo  9165  axrepnd  10208  axunnd  10210  fzpreddisj  13161  sadadd2lem2  16009  smumullem  16051  nndvdslegcd  16064  divgcdnn  16074  sqgcd  16122  coprm  16268  isnmnd  18177  nfimdetndef  21486  mdetfval1  21487  ibladdlem  24717  lgsval2lem  26188  lgsval4a  26200  lgsdilem  26205  2sqcoprm  26316  addsqn2reurex2  26326  nbgrnself  27447  wwlks  27919  iswspthsnon  27940  clwwlknon1nloop  28182  clwwlknon1le1  28184  nfrgr2v  28355  hashxpe  30847  acycgr0v  32823  prclisacycgr  32826  fmlasucdisj  33074  frxp2  33528  frxp3  33534  nosepdmlem  33623  nodenselem8  33631  nosupbnd2lem1  33655  dfrdg4  33990  finxpreclem3  35301  finxpreclem5  35303  ibladdnclem  35570  dihatlat  39085  xppss12  39917  jm2.23  40521  ltnelicc  42710  limciccioolb  42837  dvmptfprodlem  43160  stoweidlem26  43242  fourierdlem12  43335  fourierdlem42  43365  divgcdoddALTV  44807