Theorem intnan 492

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

This proof depends on syntax axioms:  ¬ wn 3   ∧ 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:  bianfi  543  noel  4291  uni0  4903  axnulALT  5269  axnul  5270  cnv0  5871  cnv0OLD  5872  imadif  6624  poxp3  8152  1div0  11888  xrltnr  13160  nltmnf  13170  0nelfz1  13587  smu01  16566  3lcm2e6woprm  16695  6lcm4e12  16696  join0  18481  meet0  18482  nsmndex1  19012  smndex2dnrinv  19014  degenmgmnfn  19036  degenmgm2nfun  19039  zringndrg  21668  zclmncvs  25358  nolt02o  27910  nogt01o  27911  legso  28919  rgrx0ndm  30001  wwlksnext  30309  ntrl2v2e  30580  avril1  30885  helloworld  30887  topnfbey  30891  xrge00  33398  axnulALT2  35534  axsepg3ALT  35612  fmlaomn0  35919  gonan0  35921  goaln0  35922  prv0  35959  dfon2lem7  36316  nandsym1  36990  bj-inftyexpitaudisj  37906  padd01  40643  ifpdfan  44250  sucomisnotcard  44328  clsk1indlem4  44828  iblempty  46737  salexct2  47111  0nodd  48992  2nodd  48994  1neven  49060  ipolub00  49828