Theorem intnan 491

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 489	. 2 ⊢ ((𝜓 ∧ 𝜑) → 𝜑)
3	1, 2	mto 200	1 ⊢ ¬ (𝜓 ∧ 𝜑)

Syntax hints:  ¬ wn 3   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  bianfi  542  noel  4291  uni0  4901  axnulALT  5267  axnul  5268  cnv0  5869  cnv0OLD  5870  imadif  6620  poxp3  8142  1div0  11868  xrltnr  13139  nltmnf  13149  0nelfz1  13566  smu01  16539  3lcm2e6woprm  16668  6lcm4e12  16669  join0  18454  meet0  18455  nsmndex1  18970  smndex2dnrinv  18972  zringndrg  21618  zclmncvs  25307  nolt02o  27859  nogt01o  27860  legso  28868  rgrx0ndm  29943  wwlksnext  30242  ntrl2v2e  30509  avril1  30814  helloworld  30816  topnfbey  30820  xrge00  33334  axnulALT2  35471  axsepg3ALT  35555  fmlaomn0  35882  gonan0  35884  goaln0  35885  prv0  35922  dfon2lem7  36279  nandsym1  36933  bj-inftyexpitaudisj  37849  padd01  40585  ifpdfan  44192  sucomisnotcard  44270  clsk1indlem4  44770  iblempty  46679  salexct2  47053  0nodd  48935  2nodd  48937  1neven  49003  ipolub00  49771