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  4279  uni0  4879  axnulALT  5239  axnul  5240  cnv0  6095  cnv0OLD  6096  imadif  6574  poxp3  8091  1div0  11798  xrltnr  13059  nltmnf  13069  0nelfz1  13486  smu01  16444  3lcm2e6woprm  16573  6lcm4e12  16574  join0  18358  meet0  18359  nsmndex1  18873  smndex2dnrinv  18875  zringndrg  21456  zclmncvs  25124  nolt02o  27678  nogt01o  27679  legso  28686  rgrx0ndm  29682  wwlksnext  29981  ntrl2v2e  30248  avril1  30553  helloworld  30555  topnfbey  30559  xrge00  33094  axnulALT2  35245  axsepg2ALT  35247  fmlaomn0  35593  gonan0  35595  goaln0  35596  prv0  35633  dfon2lem7  35990  nandsym1  36625  bj-inftyexpitaudisj  37532  padd01  40268  ifpdfan  43908  sucomisnotcard  43986  clsk1indlem4  44486  iblempty  46408  salexct2  46782  0nodd  48643  2nodd  48645  1neven  48711  ipolub00  49465