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  4284  uni0  4896  axnulALT  5261  axnul  5262  cnv0  5863  cnv0OLD  5864  imadif  6617  poxp3  8148  1div0  11897  xrltnr  13170  nltmnf  13180  0nelfz1  13597  smu01  16576  3lcm2e6woprm  16705  6lcm4e12  16706  join0  18491  meet0  18492  nsmndex1  19025  smndex2dnrinv  19027  degenmgmnfn  19049  degenmgm2nfun  19052  zringndrg  21681  zclmncvs  25376  nolt02o  27931  nogt01o  27932  legso  28941  rgrx0ndm  30053  wwlksnext  30361  ntrl2v2e  30638  avril1  30943  helloworld  30945  topnfbey  30949  xrge00  33454  axnulALT2  35590  axsepg3ALT  35668  fmlaomn0  35969  gonan0  35971  goaln0  35972  prv0  36009  dfon2lem7  36366  nandsym1  37041  bj-inftyexpitaudisj  37957  padd01  40684  ifpdfan  44306  sucomisnotcard  44384  clsk1indlem4  44884  iblempty  46793  salexct2  47167  0nodd  49085  2nodd  49087  1neven  49153  ipolub00  49919