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  4248  noel  4283  axnulALT  5194  axnul  5195  cnv0  5985  imadif  6424  xrltnr  12501  nltmnf  12511  0nelfz1  12916  smu01  15818  3lcm2e6woprm  15942  6lcm4e12  15943  meet0  17730  join0  17731  nsmndex1  18061  smndex2dnrinv  18063  zringndrg  20620  zclmncvs  23735  legso  26371  rgrx0ndm  27361  wwlksnext  27657  ntrl2v2e  27921  avril1  28226  helloworld  28228  topnfbey  28232  xrge00  30680  fmlaomn0  32644  gonan0  32646  goaln0  32647  prv0  32684  dfon2lem7  33041  nolt02o  33206  nandsym1  33777  subsym1  33782  bj-inftyexpitaudisj  34503  padd01  36979  ifpdfan  39922  clsk1indlem4  40484  iblempty  42340  salexct2  42712  0nodd  44162  2nodd  44164  1neven  44288