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 200	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 210  df-an 400

This theorem is referenced by:  bianfi  537  indifdir  4210  noel  4247  axnulALT  5172  axnul  5173  cnv0  5966  imadif  6408  xrltnr  12502  nltmnf  12512  0nelfz1  12921  smu01  15825  3lcm2e6woprm  15949  6lcm4e12  15950  meet0  17739  join0  17740  nsmndex1  18070  smndex2dnrinv  18072  zringndrg  20183  zclmncvs  23753  legso  26393  rgrx0ndm  27383  wwlksnext  27679  ntrl2v2e  27943  avril1  28248  helloworld  28250  topnfbey  28254  xrge00  30720  fmlaomn0  32750  gonan0  32752  goaln0  32753  prv0  32790  dfon2lem7  33147  nolt02o  33312  nandsym1  33883  subsym1  33888  bj-inftyexpitaudisj  34620  padd01  37107  ifpdfan  40174  clsk1indlem4  40747  iblempty  42607  salexct2  42979  0nodd  44430  2nodd  44432  1neven  44556