Theorem intnan 486

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

Syntax hints:  ¬ wn 3   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bianfi  533  noel  4297  axnulALT  5254  axnul  5255  cnv0  6101  imadif  6584  poxp3  8106  1div0  11813  xrltnr  13055  nltmnf  13065  0nelfz1  13480  smu01  16432  3lcm2e6woprm  16561  6lcm4e12  16562  join0  18340  meet0  18341  nsmndex1  18816  smndex2dnrinv  18818  zringndrg  21354  zclmncvs  25024  nolt02o  27583  nogt01o  27584  legso  28502  rgrx0ndm  29497  wwlksnext  29796  ntrl2v2e  30060  avril1  30365  helloworld  30367  topnfbey  30371  xrge00  32926  axsepg2ALT  35046  fmlaomn0  35350  gonan0  35352  goaln0  35353  prv0  35390  dfon2lem7  35750  nandsym1  36383  bj-inftyexpitaudisj  37166  padd01  39778  ifpdfan  43428  sucomisnotcard  43506  clsk1indlem4  44006  iblempty  45936  salexct2  46310  0nodd  48131  2nodd  48133  1neven  48199  ipolub00  48954