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  4344  axnulALT  5310  axnul  5311  cnv0  6163  imadif  6652  poxp3  8174  1div0  11920  xrltnr  13159  nltmnf  13169  0nelfz1  13580  smu01  16520  3lcm2e6woprm  16649  6lcm4e12  16650  join0  18463  meet0  18464  nsmndex1  18939  smndex2dnrinv  18941  zringndrg  21497  zclmncvs  25196  nolt02o  27755  nogt01o  27756  legso  28622  rgrx0ndm  29626  wwlksnext  29923  ntrl2v2e  30187  avril1  30492  helloworld  30494  topnfbey  30498  xrge00  33000  axsepg2ALT  35076  fmlaomn0  35375  gonan0  35377  goaln0  35378  prv0  35415  dfon2lem7  35771  nandsym1  36405  bj-inftyexpitaudisj  37188  padd01  39794  ifpdfan  43456  sucomisnotcard  43534  clsk1indlem4  44034  iblempty  45921  salexct2  46295  0nodd  48014  2nodd  48016  1neven  48082  ipolub00  48782