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  4301  axnulALT  5259  axnul  5260  cnv0  6113  imadif  6600  poxp3  8129  1div0  11837  xrltnr  13079  nltmnf  13089  0nelfz1  13504  smu01  16456  3lcm2e6woprm  16585  6lcm4e12  16586  join0  18364  meet0  18365  nsmndex1  18840  smndex2dnrinv  18842  zringndrg  21378  zclmncvs  25048  nolt02o  27607  nogt01o  27608  legso  28526  rgrx0ndm  29521  wwlksnext  29823  ntrl2v2e  30087  avril1  30392  helloworld  30394  topnfbey  30398  xrge00  32953  axsepg2ALT  35073  fmlaomn0  35377  gonan0  35379  goaln0  35380  prv0  35417  dfon2lem7  35777  nandsym1  36410  bj-inftyexpitaudisj  37193  padd01  39805  ifpdfan  43455  sucomisnotcard  43533  clsk1indlem4  44033  iblempty  45963  salexct2  46337  0nodd  48158  2nodd  48160  1neven  48226  ipolub00  48981