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  1508  pr1eqbg  4817  iresn0n0  6064  frxp2  8198  frxp3  8205  wemappo  9580  axrepnd  10718  axunnd  10720  fzpreddisj  13747  sadadd2lem2  16664  smumullem  16706  nndvdslegcd  16719  divgcdnn  16731  sqgcd  16780  coprm  16931  isnmnd  18977  nfimdetndef  22959  mdetfval1  22960  ibladdlem  26195  lgsval2lem  27691  lgsval4a  27703  lgsdilem  27708  2sqcoprm  27819  addsqn2reurex2  27829  nosepdmlem  28097  nodenselem8  28105  nosupbnd2lem1  28129  pw2cut2  28905  nbgrnself  29997  wwlks  30481  iswspthsnon  30502  clwwlknon1nloop  30747  clwwlknon1le1  30749  nfrgr2v  30930  tpssad  33233  hashxpe  33495  esplyind  34318  j0ltaleph  36049  acycgr0v  36111  prclisacycgr  36114  fmlasucdisj  36372  dfrdg4  36930  nmulprop  37154  finxpreclem3  38584  finxpreclem5  38586  ibladdnclem  38862  dihatlat  42657  xppss12  43550  jm2.23  44269  rexanuz2nf  46775  ltnelicc  46782  limciccioolb  46906  dvmptfprodlem  47227  stoweidlem26  47309  fourierdlem12  47402  fourierdlem42  47432  divgcdoddALTV  49053  parhomne2  51085