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  4290  uni0  4891  axnulALT  5249  axnul  5250  cnv0  6097  cnv0OLD  6098  imadif  6576  poxp3  8092  1div0  11796  xrltnr  13033  nltmnf  13043  0nelfz1  13459  smu01  16413  3lcm2e6woprm  16542  6lcm4e12  16543  join0  18326  meet0  18327  nsmndex1  18838  smndex2dnrinv  18840  zringndrg  21423  zclmncvs  25104  nolt02o  27663  nogt01o  27664  legso  28671  rgrx0ndm  29667  wwlksnext  29966  ntrl2v2e  30233  avril1  30538  helloworld  30540  topnfbey  30544  xrge00  33096  axsepg2ALT  35239  fmlaomn0  35584  gonan0  35586  goaln0  35587  prv0  35624  dfon2lem7  35981  nandsym1  36616  bj-inftyexpitaudisj  37410  padd01  40071  ifpdfan  43707  sucomisnotcard  43785  clsk1indlem4  44285  iblempty  46209  salexct2  46583  0nodd  48416  2nodd  48418  1neven  48484  ipolub00  49238