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  4318  axnulALT  5279  axnul  5280  cnv0  6134  imadif  6625  poxp3  8154  1div0  11901  xrltnr  13140  nltmnf  13150  0nelfz1  13565  smu01  16510  3lcm2e6woprm  16639  6lcm4e12  16640  join0  18420  meet0  18421  nsmndex1  18896  smndex2dnrinv  18898  zringndrg  21434  zclmncvs  25105  nolt02o  27664  nogt01o  27665  legso  28583  rgrx0ndm  29578  wwlksnext  29880  ntrl2v2e  30144  avril1  30449  helloworld  30451  topnfbey  30455  xrge00  33012  axsepg2ALT  35119  fmlaomn0  35417  gonan0  35419  goaln0  35420  prv0  35457  dfon2lem7  35812  nandsym1  36445  bj-inftyexpitaudisj  37228  padd01  39835  ifpdfan  43457  sucomisnotcard  43535  clsk1indlem4  44035  iblempty  45961  salexct2  46335  0nodd  48112  2nodd  48114  1neven  48180  ipolub00  48934