Theorem intnanrd 489

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

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

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 207  df-an 396

This theorem is referenced by:  bianfd  534  3bior1fand  1475  pr1eqbg  4862  iresn0n0  6074  fvmptopabOLD  7488  frxp2  8168  frxp3  8175  wemappo  9587  axrepnd  10632  axunnd  10634  fzpreddisj  13610  sadadd2lem2  16484  smumullem  16526  nndvdslegcd  16539  divgcdnn  16549  sqgcd  16596  coprm  16745  isnmnd  18764  nfimdetndef  22611  mdetfval1  22612  ibladdlem  25870  lgsval2lem  27366  lgsval4a  27378  lgsdilem  27383  2sqcoprm  27494  addsqn2reurex2  27504  nosepdmlem  27743  nodenselem8  27751  nosupbnd2lem1  27775  nbgrnself  29391  wwlks  29865  iswspthsnon  29886  clwwlknon1nloop  30128  clwwlknon1le1  30130  nfrgr2v  30301  hashxpe  32817  acycgr0v  35133  prclisacycgr  35136  fmlasucdisj  35384  dfrdg4  35933  finxpreclem3  37376  finxpreclem5  37378  ibladdnclem  37663  dihatlat  41317  xppss12  42247  jm2.23  42985  rexanuz2nf  45443  ltnelicc  45450  limciccioolb  45577  dvmptfprodlem  45900  stoweidlem26  45982  fourierdlem12  46075  fourierdlem42  46105  divgcdoddALTV  47607