Theorem intnan 486

Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)

Hypothesis

Ref	Expression
intnan.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
intnan	⊢ ¬ (𝜓 ∧ 𝜑)

Proof of Theorem intnan

Step	Hyp	Ref	Expression
1		intnan.1	. 2 ⊢ ¬ 𝜑
2		simpr 484	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 197	1 ⊢ ¬ (𝜓 ∧ 𝜑)

Syntax hints:  ¬ wn 3   ∧ 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:  bianfi  533  noel  4291  axnulALT  5246  axnul  5247  cnv0  6093  imadif  6570  poxp3  8090  1div0  11798  xrltnr  13040  nltmnf  13050  0nelfz1  13465  smu01  16416  3lcm2e6woprm  16545  6lcm4e12  16546  join0  18328  meet0  18329  nsmndex1  18806  smndex2dnrinv  18808  zringndrg  21394  zclmncvs  25065  nolt02o  27624  nogt01o  27625  legso  28563  rgrx0ndm  29558  wwlksnext  29857  ntrl2v2e  30121  avril1  30426  helloworld  30428  topnfbey  30432  xrge00  32987  axsepg2ALT  35069  fmlaomn0  35382  gonan0  35384  goaln0  35385  prv0  35422  dfon2lem7  35782  nandsym1  36415  bj-inftyexpitaudisj  37198  padd01  39810  ifpdfan  43459  sucomisnotcard  43537  clsk1indlem4  44037  iblempty  45966  salexct2  46340  0nodd  48174  2nodd  48176  1neven  48242  ipolub00  48997