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  4287  uni0  4888  axnulALT  5246  axnul  5247  cnv0  6094  cnv0OLD  6095  imadif  6573  poxp3  8089  1div0  11787  xrltnr  13024  nltmnf  13034  0nelfz1  13450  smu01  16404  3lcm2e6woprm  16533  6lcm4e12  16534  join0  18317  meet0  18318  nsmndex1  18829  smndex2dnrinv  18831  zringndrg  21414  zclmncvs  25095  nolt02o  27654  nogt01o  27655  legso  28597  rgrx0ndm  29593  wwlksnext  29892  ntrl2v2e  30159  avril1  30464  helloworld  30466  topnfbey  30470  xrge00  33024  axsepg2ALT  35167  fmlaomn0  35506  gonan0  35508  goaln0  35509  prv0  35546  dfon2lem7  35903  nandsym1  36538  bj-inftyexpitaudisj  37322  padd01  39983  ifpdfan  43623  sucomisnotcard  43701  clsk1indlem4  44201  iblempty  46125  salexct2  46499  0nodd  48332  2nodd  48334  1neven  48400  ipolub00  49154