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  4278  uni0  4878  axnulALT  5239  axnul  5240  cnv0  6103  cnv0OLD  6104  imadif  6582  poxp3  8100  1div0  11809  xrltnr  13070  nltmnf  13080  0nelfz1  13497  smu01  16455  3lcm2e6woprm  16584  6lcm4e12  16585  join0  18369  meet0  18370  nsmndex1  18884  smndex2dnrinv  18886  zringndrg  21448  zclmncvs  25115  nolt02o  27659  nogt01o  27660  legso  28667  rgrx0ndm  29662  wwlksnext  29961  ntrl2v2e  30228  avril1  30533  helloworld  30535  topnfbey  30539  xrge00  33074  axnulALT2  35224  axsepg2ALT  35226  fmlaomn0  35572  gonan0  35574  goaln0  35575  prv0  35612  dfon2lem7  35969  nandsym1  36604  bj-inftyexpitaudisj  37519  padd01  40257  ifpdfan  43893  sucomisnotcard  43971  clsk1indlem4  44471  iblempty  46393  salexct2  46767  0nodd  48646  2nodd  48648  1neven  48714  ipolub00  49468