Theorem intnan 490

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

Syntax hints:  ¬ wn 3   ∧ wa 399

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 400

This theorem is referenced by:  bianfi  541  noel  4288  uni0  4891  axnulALT  5251  axnul  5252  cnv0  5851  cnv0OLD  5852  imadif  6600  poxp3  8124  1div0  11840  xrltnr  13115  nltmnf  13125  0nelfz1  13542  smu01  16511  3lcm2e6woprm  16640  6lcm4e12  16641  join0  18426  meet0  18427  nsmndex1  18941  smndex2dnrinv  18943  zringndrg  21508  zclmncvs  25198  nolt02o  27747  nogt01o  27748  legso  28756  rgrx0ndm  29751  wwlksnext  30050  ntrl2v2e  30317  avril1  30622  helloworld  30624  topnfbey  30628  xrge00  33153  axnulALT2  35338  axsepg3ALT  35399  fmlaomn0  35701  gonan0  35703  goaln0  35704  prv0  35741  dfon2lem7  36098  nandsym1  36743  bj-inftyexpitaudisj  37658  padd01  40396  ifpdfan  44003  sucomisnotcard  44081  clsk1indlem4  44581  iblempty  46500  salexct2  46874  0nodd  48753  2nodd  48755  1neven  48821  ipolub00  49575