Theorem intnan 492

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

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bianfi  543  noelOLD  4283  uni0  4895  axnulALT  5257  axnul  5258  cnv0  5862  cnv0OLD  5863  imadif  6629  poxp3  8173  1div0  11982  xrltnr  13255  nltmnf  13265  0nelfz1  13683  smu01  16665  3lcm2e6woprm  16799  6lcm4e12  16800  join0  18586  meet0  18587  nsmndex1  19121  smndex2dnrinv  19123  degenmgmnfn  19145  degenmgm2nfun  19148  zringndrg  21783  zclmncvs  25478  nolt02o  28061  nogt01o  28062  legso  29071  rgrx0ndm  30183  wwlksnext  30491  ntrl2v2e  30768  avril1  31073  helloworld  31075  topnfbey  31079  xrge00  33625  axnulALT2  35764  axsepg3ALT  35870  fmlaomn0  36245  gonan0  36247  goaln0  36248  prv0  36285  dfon2lem7  36647  nandsym1  37306  bj-inftyexpitaudisj  38235  padd01  40977  ifpdfan  44576  sucomisnotcard  44654  clsk1indlem4  45153  iblempty  47083  salexct2  47457  0nodd  49375  2nodd  49377  1neven  49443  elif0  50030  ipolub00  50215