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  4360  noelOLD  4361  axnulALT  5322  axnul  5323  cnv0  6172  imadif  6662  poxp3  8191  1div0  11949  xrltnr  13182  nltmnf  13192  0nelfz1  13603  smu01  16532  3lcm2e6woprm  16662  6lcm4e12  16663  join0  18475  meet0  18476  nsmndex1  18948  smndex2dnrinv  18950  zringndrg  21502  zclmncvs  25201  nolt02o  27758  nogt01o  27759  legso  28625  rgrx0ndm  29629  wwlksnext  29926  ntrl2v2e  30190  avril1  30495  helloworld  30497  topnfbey  30501  xrge00  32998  axsepg2ALT  35059  fmlaomn0  35358  gonan0  35360  goaln0  35361  prv0  35398  dfon2lem7  35753  nandsym1  36388  bj-inftyexpitaudisj  37171  padd01  39768  ifpdfan  43428  sucomisnotcard  43506  clsk1indlem4  44006  iblempty  45886  salexct2  46260  0nodd  47893  2nodd  47895  1neven  47961  ipolub00  48665