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  4283  axnulALT  5237  axnul  5238  cnv0  6082  imadif  6560  poxp3  8075  1div0  11771  xrltnr  13013  nltmnf  13023  0nelfz1  13438  smu01  16392  3lcm2e6woprm  16521  6lcm4e12  16522  join0  18304  meet0  18305  nsmndex1  18816  smndex2dnrinv  18818  zringndrg  21400  zclmncvs  25070  nolt02o  27629  nogt01o  27630  legso  28572  rgrx0ndm  29567  wwlksnext  29866  ntrl2v2e  30130  avril1  30435  helloworld  30437  topnfbey  30441  xrge00  32987  axsepg2ALT  35087  fmlaomn0  35426  gonan0  35428  goaln0  35429  prv0  35466  dfon2lem7  35823  nandsym1  36456  bj-inftyexpitaudisj  37239  padd01  39850  ifpdfan  43499  sucomisnotcard  43577  clsk1indlem4  44077  iblempty  46003  salexct2  46377  0nodd  48201  2nodd  48203  1neven  48269  ipolub00  49024