Theorem intnanrd 492

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

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

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 399

This theorem is referenced by:  bianfd  537  3bior1fand  1472  pr1eqbg  4789  iresn0n0  5925  fvmptopab  7211  wemappo  9015  axrepnd  10018  axunnd  10020  fzpreddisj  12959  sadadd2lem2  15801  smumullem  15843  nndvdslegcd  15856  divgcdnn  15865  sqgcd  15911  coprm  16057  isnmnd  17917  nfimdetndef  21200  mdetfval1  21201  ibladdlem  24422  lgsval2lem  25885  lgsval4a  25897  lgsdilem  25902  2sqcoprm  26013  addsqn2reurex2  26023  nbgrnself  27143  wwlks  27615  iswspthsnon  27636  clwwlknon1nloop  27880  clwwlknon1le1  27882  nfrgr2v  28053  hashxpe  30531  acycgr0v  32397  prclisacycgr  32400  fmlasucdisj  32648  nosepdmlem  33189  nodenselem8  33197  nosupbnd2lem1  33217  dfrdg4  33414  finxpreclem3  34676  finxpreclem5  34678  ibladdnclem  34950  dihatlat  38472  xppss12  39122  jm2.23  39600  ltnelicc  41779  limciccioolb  41909  dvmptfprodlem  42236  stoweidlem26  42318  fourierdlem12  42411  fourierdlem42  42441  divgcdoddALTV  43854