Theorem intnan 487

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 485	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 198	1 ⊢ ¬ (𝜓 ∧ 𝜑)

Syntax hints:  ¬ wn 3   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  bianfi  538  noel  4266  uni0  4866  axnulALT  5226  axnul  5227  cnv0  6090  cnv0OLD  6091  imadif  6569  poxp3  8090  1div0  11800  xrltnr  13061  nltmnf  13071  0nelfz1  13488  smu01  16446  3lcm2e6woprm  16575  6lcm4e12  16576  join0  18360  meet0  18361  nsmndex1  18875  smndex2dnrinv  18877  zringndrg  21443  zclmncvs  25133  nolt02o  27677  nogt01o  27678  legso  28685  rgrx0ndm  29680  wwlksnext  29979  ntrl2v2e  30246  avril1  30551  helloworld  30553  topnfbey  30557  xrge00  33093  axnulALT2  35264  axsepg3ALT  35323  fmlaomn0  35618  gonan0  35620  goaln0  35621  prv0  35658  dfon2lem7  36015  nandsym1  36650  bj-inftyexpitaudisj  37565  padd01  40303  ifpdfan  43910  sucomisnotcard  43988  clsk1indlem4  44488  iblempty  46408  salexct2  46782  0nodd  48661  2nodd  48663  1neven  48729  ipolub00  49483