Theorem intnan 489

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

Syntax hints:  ¬ wn 3   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  bianfi  536  indifdir  4260  noel  4296  axnulALT  5201  axnul  5202  cnv0  5994  imadif  6433  xrltnr  12508  nltmnf  12518  0nelfz1  12920  smu01  15829  3lcm2e6woprm  15953  6lcm4e12  15954  meet0  17741  join0  17742  nsmndex1  18072  smndex2dnrinv  18074  zringndrg  20631  zclmncvs  23746  legso  26379  rgrx0ndm  27369  wwlksnext  27665  ntrl2v2e  27931  avril1  28236  helloworld  28238  topnfbey  28242  xrge00  30668  fmlaomn0  32632  gonan0  32634  goaln0  32635  prv0  32672  dfon2lem7  33029  nolt02o  33194  nandsym1  33765  subsym1  33770  bj-inftyexpitaudisj  34481  padd01  36941  ifpdfan  39824  clsk1indlem4  40387  iblempty  42242  salexct2  42615  0nodd  44070  2nodd  44072  1neven  44196