Theorem intnan 487

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

Syntax hints:  ¬ wn 3   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  bianfi  534  indifdirOLD  4220  noel  4265  noelOLD  4266  dfopif  4801  axnulALT  5229  axnul  5230  cnv0  6049  imadif  6525  xrltnr  12864  nltmnf  12874  0nelfz1  13284  smu01  16202  3lcm2e6woprm  16329  6lcm4e12  16330  join0  18132  meet0  18133  nsmndex1  18561  smndex2dnrinv  18563  zringndrg  20699  zclmncvs  24321  legso  26969  rgrx0ndm  27969  wwlksnext  28267  ntrl2v2e  28531  avril1  28836  helloworld  28838  topnfbey  28842  xrge00  31304  fmlaomn0  33361  gonan0  33363  goaln0  33364  prv0  33401  dfon2lem7  33774  poxp3  33805  nolt02o  33907  nogt01o  33908  nandsym1  34620  subsym1  34625  bj-inftyexpitaudisj  35385  padd01  37832  ifpdfan  41080  sucomisnotcard  41158  clsk1indlem4  41661  iblempty  43513  salexct2  43885  0nodd  45375  2nodd  45377  1neven  45501  ipolub00  46290