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  4279  uni0  4879  axnulALT  5239  axnul  5240  cnv0  6097  cnv0OLD  6098  imadif  6576  poxp3  8093  1div0  11800  xrltnr  13061  nltmnf  13071  0nelfz1  13488  smu01  16446  3lcm2e6woprm  16575  6lcm4e12  16576  join0  18360  meet0  18361  nsmndex1  18875  smndex2dnrinv  18877  zringndrg  21458  zclmncvs  25125  nolt02o  27673  nogt01o  27674  legso  28681  rgrx0ndm  29677  wwlksnext  29976  ntrl2v2e  30243  avril1  30548  helloworld  30550  topnfbey  30554  xrge00  33089  axnulALT2  35240  axsepg2ALT  35242  fmlaomn0  35588  gonan0  35590  goaln0  35591  prv0  35628  dfon2lem7  35985  nandsym1  36620  bj-inftyexpitaudisj  37535  padd01  40271  ifpdfan  43911  sucomisnotcard  43989  clsk1indlem4  44489  iblempty  46411  salexct2  46785  0nodd  48658  2nodd  48660  1neven  48726  ipolub00  49480