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  4337  axnulALT  5303  axnul  5304  cnv0  6159  imadif  6649  poxp3  8176  1div0  11923  xrltnr  13162  nltmnf  13172  0nelfz1  13584  smu01  16524  3lcm2e6woprm  16653  6lcm4e12  16654  join0  18451  meet0  18452  nsmndex1  18927  smndex2dnrinv  18929  zringndrg  21480  zclmncvs  25183  nolt02o  27741  nogt01o  27742  legso  28608  rgrx0ndm  29612  wwlksnext  29914  ntrl2v2e  30178  avril1  30483  helloworld  30485  topnfbey  30489  xrge00  33018  axsepg2ALT  35098  fmlaomn0  35396  gonan0  35398  goaln0  35399  prv0  35436  dfon2lem7  35791  nandsym1  36424  bj-inftyexpitaudisj  37207  padd01  39814  ifpdfan  43484  sucomisnotcard  43562  clsk1indlem4  44062  iblempty  45985  salexct2  46359  0nodd  48091  2nodd  48093  1neven  48159  ipolub00  48897