Theorem intnanrd 495

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bianfd  544  3bior1fand  1507  pr1eqbg  4817  iresn0n0  6050  frxp2  8142  frxp3  8149  wemappo  9521  axrepnd  10603  axunnd  10605  fzpreddisj  13628  sadadd2lem2  16540  smumullem  16582  nndvdslegcd  16595  divgcdnn  16605  sqgcd  16652  coprm  16802  isnmnd  18840  nfimdetndef  22811  mdetfval1  22812  ibladdlem  26047  lgsval2lem  27543  lgsval4a  27555  lgsdilem  27560  2sqcoprm  27671  addsqn2reurex2  27681  nosepdmlem  27919  nodenselem8  27927  nosupbnd2lem1  27951  pw2cut2  28727  nbgrnself  29819  wwlks  30303  iswspthsnon  30324  clwwlknon1nloop  30569  clwwlknon1le1  30571  nfrgr2v  30752  tpssad  33014  hashxpe  33278  esplyind  34085  acycgr0v  35727  prclisacycgr  35730  fmlasucdisj  35978  dfrdg4  36530  nmulprop  36770  finxpreclem3  38147  finxpreclem5  38149  ibladdnclem  38425  dihatlat  42207  xppss12  43099  jm2.23  43837  rexanuz2nf  46320  ltnelicc  46327  limciccioolb  46451  dvmptfprodlem  46772  stoweidlem26  46854  fourierdlem12  46947  fourierdlem42  46977  divgcdoddALTV  48598