Theorem intnan 998

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

Syntax hints:  ¬ wn 3   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  bianfi  1004  indifdir  4026  axnulALT  4939  axnul  4940  cnv0  5693  imadif  6134  xrltnr  12146  nltmnf  12156  0nelfz1  12553  smu01  15410  3lcm2e6woprm  15530  6lcm4e12  15531  meet0  17338  join0  17339  zringndrg  20040  zclmncvs  23148  legso  25693  rgrx0ndm  26699  wwlksnext  27011  ntrl2v2e  27310  avril1  27630  helloworld  27632  topnfbey  27636  xrge00  29995  dfon2lem7  31999  nolt02o  32151  nandsym1  32727  subsym1  32732  padd01  35600  ifpdfan  38312  clsk1indlem4  38844  iblempty  40684  salexct2  41060  0nodd  42320  2nodd  42322  1neven  42442