Theorem intnanrd 494

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

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

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 401

This theorem is referenced by:  bianfd  543  3bior1fand  1507  pr1eqbg  4823  iresn0n0  6058  frxp2  8141  frxp3  8148  wemappo  9512  axrepnd  10580  axunnd  10582  fzpreddisj  13603  sadadd2lem2  16509  smumullem  16551  nndvdslegcd  16564  divgcdnn  16574  sqgcd  16621  coprm  16771  isnmnd  18797  nfimdetndef  22727  mdetfval1  22728  ibladdlem  25960  lgsval2lem  27452  lgsval4a  27464  lgsdilem  27469  2sqcoprm  27580  addsqn2reurex2  27590  nosepdmlem  27828  nodenselem8  27836  nosupbnd2lem1  27860  pw2cut2  28636  nbgrnself  29690  wwlks  30165  iswspthsnon  30186  clwwlknon1nloop  30431  clwwlknon1le1  30433  nfrgr2v  30604  tpssad  32866  hashxpe  33133  esplyind  33946  acycgr0v  35621  prclisacycgr  35624  fmlasucdisj  35872  dfrdg4  36424  nmulprop  36663  finxpreclem3  38020  finxpreclem5  38022  ibladdnclem  38308  dihatlat  42089  xppss12  42981  jm2.23  43706  rexanuz2nf  46189  ltnelicc  46196  limciccioolb  46320  dvmptfprodlem  46641  stoweidlem26  46723  fourierdlem12  46816  fourierdlem42  46846  divgcdoddALTV  48430